chore: repair example

This commit is contained in:
Simon Cruanes 2018-12-13 18:40:29 -06:00
parent 1150098cd2
commit a917dc663b
5 changed files with 58 additions and 59 deletions

8
examples/dune Normal file
View file

@ -0,0 +1,8 @@
(executable
(name test_sexpr)
(libraries iter)
(flags :standard -w +a-4-42-44-48-50-58-32-60@8 -safe-string -color always)
(ocamlopt_flags :standard -O3 -color always
-unbox-closures -unbox-closures-factor 20)
)

View file

@ -1,8 +0,0 @@
(executable
((name test_sexpr)
(libraries (sequence))
(flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -safe-string -color always))
(ocamlopt_flags (:standard -O3 -color always
-unbox-closures -unbox-closures-factor 20))
))

View file

@ -1,5 +1,4 @@
(* (*
Zipperposition: a functional superposition prover for prototyping
Copyright (C) 2012 Simon Cruanes Copyright (C) 2012 Simon Cruanes
This is free software; you can redistribute it and/or This is free software; you can redistribute it and/or
@ -39,7 +38,7 @@ and iter_list f l = match l with
| x::l' -> iter f x; iter_list f l' | x::l' -> iter f x; iter_list f l'
(** Traverse. This yields a sequence of tokens *) (** Traverse. This yields a sequence of tokens *)
let traverse s = Sequence.from_iter (fun k -> iter k s) let traverse s = Iter.from_iter (fun k -> iter k s)
(** Returns the same sequence of tokens, but during iteration, if (** Returns the same sequence of tokens, but during iteration, if
the structure of the Sexpr corresponding to the sequence the structure of the Sexpr corresponding to the sequence
@ -47,7 +46,7 @@ let traverse s = Sequence.from_iter (fun k -> iter k s)
and iteration is stoped *) and iteration is stoped *)
let validate seq = let validate seq =
let depth = ref 0 in let depth = ref 0 in
Sequence.map Iter.map
(fun tok -> match tok with (fun tok -> match tok with
| `Open -> incr depth; tok | `Open -> incr depth; tok
| `Close -> if !depth = 0 | `Close -> if !depth = 0
@ -80,9 +79,9 @@ let lex input =
k (`Atom word) k (`Atom word)
end end
in in
Sequence.iter next input Iter.iter next input
in in
Sequence.from_iter seq_fun Iter.from_iter seq_fun
(** Build a Sexpr from a sequence of tokens *) (** Build a Sexpr from a sequence of tokens *)
let of_seq seq = let of_seq seq =
@ -98,7 +97,7 @@ let of_seq seq =
| _ -> assert false | _ -> assert false
in in
(* iterate on the sequence, given an empty initial stack *) (* iterate on the sequence, given an empty initial stack *)
let stack = Sequence.fold k [] seq in let stack = Iter.fold k [] seq in
(* stack should contain exactly one expression *) (* stack should contain exactly one expression *)
match stack with match stack with
| [`Expr expr] -> expr | [`Expr expr] -> expr
@ -117,7 +116,7 @@ let pp_token formatter token = match token with
let pp_tokens formatter tokens = let pp_tokens formatter tokens =
let first = ref true in let first = ref true in
let last = ref false in let last = ref false in
Sequence.iter Iter.iter
(fun token -> (fun token ->
(match token with (match token with
| `Open -> (if not !first then Format.fprintf formatter " "); first := true | `Open -> (if not !first then Format.fprintf formatter " "); first := true
@ -139,7 +138,7 @@ let pp_sexpr ?(indent=false) formatter s =
let output_seq name subexpr k = let output_seq name subexpr k =
k `Open; k `Open;
k (`Atom name); k (`Atom name);
Sequence.iter k subexpr; Iter.iter k subexpr;
k `Close k `Close
let output_str name str k = let output_str name str k =
@ -258,7 +257,7 @@ let parse_k p tokens k =
match reduce state with match reduce state with
| Bottom -> (* should not happen, unless there are too many tokens *) | Bottom -> (* should not happen, unless there are too many tokens *)
raise (ParseFailure "unexpected ')'") raise (ParseFailure "unexpected ')'")
| Push (Return _, cont) -> | Push (Return _, _cont) ->
assert false (* should be reduced *) assert false (* should be reduced *)
| Push (Zero f, cont) -> | Push (Zero f, cont) ->
let p' = f token in let p' = f token in
@ -285,7 +284,7 @@ let parse_k p tokens k =
| _ -> state | _ -> state
in in
(* iterate on the tokens *) (* iterate on the tokens *)
ignore (Sequence.fold one_step state tokens) ignore (Iter.fold one_step state tokens)
(** Parse one value *) (** Parse one value *)
let parse p tokens = let parse p tokens =
@ -301,5 +300,5 @@ let parse_seq p tokens =
let seq_fun k = let seq_fun k =
parse_k p tokens (fun x -> k x; `Continue) parse_k p tokens (fun x -> k x; `Continue)
in in
Sequence.from_iter seq_fun Iter.from_iter seq_fun

View file

@ -33,10 +33,10 @@ type token = [`Open | `Close | `Atom of string]
val iter : (token -> unit) -> t -> unit val iter : (token -> unit) -> t -> unit
(** Iterate on the S-expression, calling the callback with tokens *) (** Iterate on the S-expression, calling the callback with tokens *)
val traverse : t -> token Sequence.t val traverse : t -> token Iter.t
(** Traverse. This yields a sequence of tokens *) (** Traverse. This yields a sequence of tokens *)
val validate : token Sequence.t -> token Sequence.t val validate : token Iter.t -> token Iter.t
(** Returns the same sequence of tokens, but during iteration, if (** Returns the same sequence of tokens, but during iteration, if
the structure of the Sexpr corresponding to the sequence the structure of the Sexpr corresponding to the sequence
is wrong (bad parenthesing), Invalid_argument is raised is wrong (bad parenthesing), Invalid_argument is raised
@ -44,10 +44,10 @@ val validate : token Sequence.t -> token Sequence.t
(** {2 Text <-> tokens} *) (** {2 Text <-> tokens} *)
val lex : char Sequence.t -> token Sequence.t val lex : char Iter.t -> token Iter.t
(** Lex: create a sequence of tokens from the given sequence of chars. *) (** Lex: create a sequence of tokens from the given sequence of chars. *)
val of_seq : token Sequence.t -> t val of_seq : token Iter.t -> t
(** Build a Sexpr from a sequence of tokens, or raise Failure *) (** Build a Sexpr from a sequence of tokens, or raise Failure *)
(** {2 Printing} *) (** {2 Printing} *)
@ -55,7 +55,7 @@ val of_seq : token Sequence.t -> t
val pp_token : Format.formatter -> token -> unit val pp_token : Format.formatter -> token -> unit
(** Print a token on the given formatter *) (** Print a token on the given formatter *)
val pp_tokens : Format.formatter -> token Sequence.t -> unit val pp_tokens : Format.formatter -> token Iter.t -> unit
(** Print a sequence of Sexpr tokens on the given formatter *) (** Print a sequence of Sexpr tokens on the given formatter *)
val pp_sexpr : ?indent:bool -> Format.formatter -> t -> unit val pp_sexpr : ?indent:bool -> Format.formatter -> t -> unit
@ -64,7 +64,7 @@ val pp_sexpr : ?indent:bool -> Format.formatter -> t -> unit
(** {2 Serializing} *) (** {2 Serializing} *)
val output_seq : string -> token Sequence.t -> (token -> unit) -> unit val output_seq : string -> token Iter.t -> (token -> unit) -> unit
(** print a pair "(name @,sequence)" *) (** print a pair "(name @,sequence)" *)
val output_str : string -> string -> (token -> unit) -> unit val output_str : string -> string -> (token -> unit) -> unit
@ -124,9 +124,9 @@ val p_bool : bool parser
val many : 'a parser -> 'a list parser val many : 'a parser -> 'a list parser
val many1 : 'a parser -> 'a list parser val many1 : 'a parser -> 'a list parser
val parse : 'a parser -> token Sequence.t -> 'a val parse : 'a parser -> token Iter.t -> 'a
(** Parses exactly one value from the sequence of tokens. Raises (** Parses exactly one value from the sequence of tokens. Raises
ParseFailure if anything goes wrong. *) ParseFailure if anything goes wrong. *)
val parse_seq : 'a parser -> token Sequence.t -> 'a Sequence.t val parse_seq : 'a parser -> token Iter.t -> 'a Iter.t
(** Parses a sequence of values *) (** Parses a sequence of values *)

View file

@ -3,16 +3,16 @@
(** print a list of items using the printing function *) (** print a list of items using the printing function *)
let pp_list ?(sep=", ") pp_item formatter l = let pp_list ?(sep=", ") pp_item formatter l =
Sequence.pp_seq ~sep pp_item formatter (Sequence.of_list l) Iter.pp_seq ~sep pp_item formatter (Iter.of_list l)
(** Set of integers *) (** Set of integers *)
module ISet = Set.Make(struct type t = int let compare = compare end) module ISet = Set.Make(struct type t = int let compare = compare end)
let iset = (module ISet : Set.S with type elt = int and type t = ISet.t) let iset = (module ISet : Set.S with type elt = int and type t = ISet.t)
module OrderedString = struct type t = string let compare = compare end module OrderedString = struct type t = string let compare = compare end
module SMap = Sequence.Map.Make(OrderedString) module SMap = Iter.Map.Make(OrderedString)
let my_map = SMap.of_seq (Sequence.of_list ["1", 1; "2", 2; "3", 3; "answer", 42]) let my_map = SMap.of_seq (Iter.of_list ["1", 1; "2", 2; "3", 3; "answer", 42])
let sexpr = "(foo bar (bazz quux hello 42) world (zoo foo bar (1 2 (3 4))))" let sexpr = "(foo bar (bazz quux hello 42) world (zoo foo bar (1 2 (3 4))))"
@ -35,9 +35,9 @@ let rec sexpr_of_term t =
let f t k = match t with let f t k = match t with
| Var i -> Sexpr.output_str "var" (string_of_int i) k | Var i -> Sexpr.output_str "var" (string_of_int i) k
| Lambda t' -> Sexpr.output_seq "lambda" (sexpr_of_term t') k | Lambda t' -> Sexpr.output_seq "lambda" (sexpr_of_term t') k
| Apply (t1, t2) -> Sexpr.output_seq "apply" (Sequence.append (sexpr_of_term t1) (sexpr_of_term t2)) k | Apply (t1, t2) -> Sexpr.output_seq "apply" (Iter.append (sexpr_of_term t1) (sexpr_of_term t2)) k
| Const s -> Sexpr.output_str "const" s k | Const s -> Sexpr.output_str "const" s k
in Sequence.from_iter (f t) in Iter.from_iter (f t)
let term_parser = let term_parser =
let open Sexpr in let open Sexpr in
@ -68,61 +68,61 @@ let test_term () =
let _ = let _ =
(* lists *) (* lists *)
let l = [0;1;2;3;4;5;6] in let l = [0;1;2;3;4;5;6] in
let l' = Sequence.to_list let l' = Iter.to_list
(Sequence.filter (fun x -> x mod 2 = 0) (Sequence.of_list l)) in (Iter.filter (fun x -> x mod 2 = 0) (Iter.of_list l)) in
let l'' = Sequence.to_list let l'' = Iter.to_list
(Sequence.take 3 (Sequence.drop 1 (Sequence.of_list l))) in (Iter.take 3 (Iter.drop 1 (Iter.of_list l))) in
let h = Hashtbl.create 3 in let h = Hashtbl.create 3 in
for i = 0 to 5 do for i = 0 to 5 do
Hashtbl.add h i (i*i); Hashtbl.add h i (i*i);
done; done;
let l2 = Sequence.to_list let l2 = Iter.to_list
(Sequence.map (fun (x, y) -> (string_of_int x) ^ " -> " ^ (string_of_int y)) (Iter.map (fun (x, y) -> (string_of_int x) ^ " -> " ^ (string_of_int y))
(Sequence.of_hashtbl h)) (Iter.of_hashtbl h))
in in
let l3 = Sequence.to_list (Sequence.rev (Sequence.int_range ~start:0 ~stop:42)) in let l3 = Iter.to_list (Iter.rev (Iter.int_range ~start:0 ~stop:42)) in
let set = List.fold_left (fun set x -> ISet.add x set) ISet.empty [4;3;100;42] in let set = List.fold_left (fun set x -> ISet.add x set) ISet.empty [4;3;100;42] in
let l4 = Sequence.to_list (Sequence.of_set iset set) in let l4 = Iter.to_list (Iter.of_set iset set) in
Format.printf "l=@[<h>[%a]@]@." (pp_list Format.pp_print_int) l; Format.printf "l=@[<h>[%a]@]@." (pp_list Format.pp_print_int) l;
Format.printf "l'=@[<h>[%a]@]@." (pp_list Format.pp_print_int) l'; Format.printf "l'=@[<h>[%a]@]@." (pp_list Format.pp_print_int) l';
Format.printf "l''=@[<h>[%a]@]@." (pp_list Format.pp_print_int) l''; Format.printf "l''=@[<h>[%a]@]@." (pp_list Format.pp_print_int) l'';
Format.printf "l2=@[<h>[%a]@]@." (pp_list Format.pp_print_string) l2; Format.printf "l2=@[<h>[%a]@]@." (pp_list Format.pp_print_string) l2;
Format.printf "l3=@[<h>[%a]@]@." (pp_list Format.pp_print_int) l3; Format.printf "l3=@[<h>[%a]@]@." (pp_list Format.pp_print_int) l3;
Format.printf "s={@[<h>%a@]}@." (Sequence.pp_seq Format.pp_print_int) (Sequence.of_set iset set); Format.printf "s={@[<h>%a@]}@." (Iter.pp_seq Format.pp_print_int) (Iter.of_set iset set);
Format.printf "l4=@[<h>[%a]@]@." (pp_list Format.pp_print_int) l4; Format.printf "l4=@[<h>[%a]@]@." (pp_list Format.pp_print_int) l4;
Format.printf "l3[:5]+l4=@[<h>[%a]@]@." (Sequence.pp_seq Format.pp_print_int) Format.printf "l3[:5]+l4=@[<h>[%a]@]@." (Iter.pp_seq Format.pp_print_int)
(Sequence.of_array (Iter.of_array
(Sequence.to_array (Sequence.append (Iter.to_array (Iter.append
(Sequence.take 5 (Sequence.of_list l3)) (Sequence.of_list l4)))); (Iter.take 5 (Iter.of_list l3)) (Iter.of_list l4))));
(* sequence, persistent, etc *) (* sequence, persistent, etc *)
let seq = Sequence.int_range ~start:0 ~stop:100000 in let seq = Iter.int_range ~start:0 ~stop:100000 in
let seq' = Sequence.persistent seq in let seq' = Iter.persistent seq in
let stream = Sequence.to_stream seq' in let stream = Iter.to_stream seq' in
Format.printf "test length [0..100000]: persistent1 %d, stream %d, persistent2 %d" Format.printf "test length [0..100000]: persistent1 %d, stream %d, persistent2 %d"
(Sequence.length seq') (Sequence.length (Sequence.of_stream stream)) (Sequence.length seq'); (Iter.length seq') (Iter.length (Iter.of_stream stream)) (Iter.length seq');
(* maps *) (* maps *)
Format.printf "@[<h>map: %a@]@." Format.printf "@[<h>map: %a@]@."
(Sequence.pp_seq (fun formatter (k,v) -> Format.fprintf formatter "\"%s\" -> %d" k v)) (Iter.pp_seq (fun formatter (k,v) -> Format.fprintf formatter "\"%s\" -> %d" k v))
(SMap.to_seq my_map); (SMap.to_seq my_map);
let module MyMapSeq = Sequence.Map.Adapt(Map.Make(OrderedString)) in let module MyMapSeq = Iter.Map.Adapt(Map.Make(OrderedString)) in
let my_map' = MyMapSeq.of_seq (Sequence.of_list ["1", 1; "2", 2; "3", 3; "answer", 42]) in let my_map' = MyMapSeq.of_seq (Iter.of_list ["1", 1; "2", 2; "3", 3; "answer", 42]) in
Format.printf "@[<h>map: %a@]@." Format.printf "@[<h>map: %a@]@."
(Sequence.pp_seq (fun formatter (k,v) -> Format.fprintf formatter "\"%s\" -> %d" k v)) (Iter.pp_seq (fun formatter (k,v) -> Format.fprintf formatter "\"%s\" -> %d" k v))
(MyMapSeq.to_seq my_map'); (MyMapSeq.to_seq my_map');
(* sum *) (* sum *)
let n = 1000000 in let n = 1000000 in
let sum = Sequence.fold (+) 0 (Sequence.take n (Sequence.repeat 1)) in let sum = Iter.fold (+) 0 (Iter.take n (Iter.repeat 1)) in
Format.printf "%dx1 = %d@." n sum; Format.printf "%dx1 = %d@." n sum;
assert (n=sum); assert (n=sum);
(* sexpr *) (* sexpr *)
let s = Sexpr.of_seq (Sexpr.lex (Sequence.of_str sexpr)) in let s = Sexpr.of_seq (Sexpr.lex (Iter.of_str sexpr)) in
let s = Sexpr.of_seq (Sequence.map let s = Sexpr.of_seq (Iter.map
(function | `Atom s -> `Atom (String.capitalize s) | tok -> tok) (function | `Atom s -> `Atom (String.capitalize_ascii s) | tok -> tok)
(Sexpr.traverse s)) (Sexpr.traverse s))
in in
Format.printf "@[<hov2>transform @[<h>%s@] into @[<h>%a@]@]@." sexpr (Sexpr.pp_sexpr ~indent:false) s; Format.printf "@[<hov2>transform @[<h>%s@] into @[<h>%a@]@]@." sexpr (Sexpr.pp_sexpr ~indent:false) s;
Format.printf "@[<hv2> cycle:%a@]@." Sexpr.pp_tokens Format.printf "@[<hv2> cycle:%a@]@." Sexpr.pp_tokens
(Sequence.concat (Sequence.take 10 (Sequence.repeat (Sexpr.traverse s)))); (Iter.concat (Iter.take 10 (Iter.repeat (Sexpr.traverse s))));
(* sexpr parsing/printing *) (* sexpr parsing/printing *)
for i = 0 to 20 do for i = 0 to 20 do
Format.printf "%d-th term test@." i; Format.printf "%d-th term test@." i;