]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Clean-up to examples. Removed tests.
authoracondolu <andrea.condoluci@unibo.it>
Tue, 29 May 2018 09:03:13 +0000 (11:03 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Wed, 30 May 2018 13:28:24 +0000 (15:28 +0200)
ocaml/andrea.ml

index f1cfc0177cae19ae3843c4a8498b0b6adbe23911..8066a3d79f76e5a845cdaa67de2212afdcf14834 100644 (file)
@@ -327,79 +327,41 @@ let rec conv_join = function
  | x::xs -> conv_join xs ^ " ("^ x ^")"\r
 ;;\r
 \r
-let _ = exec\r
+let auto' a b = auto (problem_of a (conv_join b));;\r
+\r
+(* Example usage of exec, interactive:\r
+\r
+exec\r
  "x x"\r
  (conv_join["x y"; "y y"; "y x"])\r
  [ step 0 0; eat ]\r
 ;;\r
 \r
-auto (problem_of "x x" "@ (x y) (y y) (y x)");;\r
-auto (problem_of "x y" "@ (x (_. x)) (y z) (y x)");;\r
-auto (problem_of "a (x. x b) (x. x c)" "@ (a (x. b b) @) (a @ c) (a (x. x x) a) (a (a a a) (a c c))");;\r
-\r
 interactive "x y"\r
-"@ (x x) (y x) (y z)" [step 0 0; step 0 1; eat] ;;\r
+ "@ (x x) (y x) (y z)" [step 0 0; step 0 1; eat]\r
+;;\r
+\r
+*)\r
 \r
-auto (problem_of "x (y. x y y)" "x (y. x y x)");;\r
+auto' "x x" ["x y"; "y y"; "y x"] ;;\r
+auto' "x y" ["x (_. x)"; "y z"; "y x"] ;;\r
+auto' "a (x. x b) (x. x c)" ["a (x. b b) @"; "a @ c"; "a (x. x x) a"; "a (a a a) (a c c)"] ;;\r
 \r
-auto (problem_of "x a a a a" (conv_join[\r
+auto' "x (y. x y y)" ["x (y. x y x)"] ;;\r
+\r
+auto' "x a a a a" [\r
  "x b a a a";\r
  "x a b a a";\r
  "x a a b a";\r
  "x a a a b";\r
-]));\r
+] ;;\r
 \r
 (* Controesempio ad usare un conto dei lambda che non considere le permutazioni *)\r
-auto (problem_of "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" (conv_join[\r
+auto' "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [\r
  "x a a a a (_. a) b b b";\r
  "x a a a a (_. _. _. _. x. y. x y)";\r
-]));\r
+] ;;\r
 \r
 \r
 print_hline();\r
 print_endline "ALL DONE. "\r
-\r
-(* TEMPORARY TESTING FACILITY BELOW HERE *)\r
-\r
-let acaso l =\r
-    let n = Random.int (List.length l) in\r
-    List.nth l n\r
-;;\r
-\r
-let acaso2 l1 l2 =\r
-  let n1 = List.length l1 in\r
-  let n = Random.int (n1 + List.length l2) in\r
-  if n >= n1 then List.nth l2 (n - n1) else List.nth l1 n\r
-;;\r
-\r
-let gen n vars =\r
-  let rec aux n inerts lams =\r
-    if n = 0 then List.hd inerts, List.hd (Util.sort_uniq (List.tl inerts))\r
-    else let inerts, lams = if Random.int 2 = 0\r
-      then inerts, ("(" ^ acaso vars ^ ". " ^ acaso2 inerts lams ^ ")") :: lams\r
-      else ("(" ^ acaso inerts ^ " " ^ acaso2 inerts lams^ ")") :: inerts, lams\r
-    in aux (n-1) inerts lams\r
-  in aux (2*n) vars []\r
-;;\r
-\r
-let f () =\r
-  let complex = 200 in\r
-  let vars = ["x"; "y"; "z"; "v" ; "w"; "a"; "b"; "c"] in\r
-  gen complex vars\r
-\r
-  let rec repeat f n =\r
-    prerr_endline "\n########################### NEW TEST ###########################";\r
-    f () ;\r
-    if n > 0 then repeat f (n-1)\r
-  ;;\r
-\r
-\r
-let main () =\r
- Random.self_init ();\r
- repeat (fun _ ->\r
-   let div, conv = f () in\r
-   auto (problem_of div conv)\r
- ) 100;\r
-;;\r
-\r
-(* main ();; *)\r