Changed coding style

No space before ;
; at the end of every top-level statement

examples/compute/examples/and_not/ex_and_notScript.sml

@@ -3,14 +3,14 @@
 (*  a variable or its negation                                               *)
 (* ------------------------------------------------------------------------- *)
 
-open HolKernel Parse boolLib bossLib ;
-open bir_basicTheory bir_envTheory ;
-open bir_binexpTheory bir_ifthenelseTheory bir_unaryexpTheory ;
-open bir_computeTheory ;
-open wordsLib ;
+open HolKernel Parse boolLib bossLib;
+open bir_basicTheory bir_envTheory;
+open bir_binexpTheory bir_ifthenelseTheory bir_unaryexpTheory;
+open bir_computeTheory;
+open wordsLib;
 
 
-val _ = new_theory "ex_and_not" ;
+val _ = new_theory "ex_and_not";
 
 (* The variables used in the condition. They will be booleans *)
 Definition var_cond1_def:
@@ -79,4 +79,4 @@ QED
 
 
 
-val _ = export_theory () ;
+val _ = export_theory ();

examples/compute/examples/increment/ex_incrementLib.sig

@@ -1,9 +1,9 @@
 signature ex_incrementLib =
 sig
 
-  include Abbrev ;
+  include Abbrev;
 
-  val generate_bigger_inc : term -> int -> term ;
-  val benchmark : unit -> unit ;
+  val generate_bigger_inc : term -> int -> term;
+  val benchmark : unit -> unit;
 
 end

examples/compute/examples/increment/ex_incrementLib.sml

@@ -6,52 +6,52 @@ structure ex_incrementLib :> ex_incrementLib =
 struct
 
 open HolKernel Parse bossLib boolLib;
-open bir_basicTheory ;
-open ex_incrementTheory ;
-open bir_computeLib ;
+open bir_basicTheory;
+open ex_incrementTheory;
+open bir_computeLib;
 
 
 fun generate_bigger_inc (term:term) (n:int) : term =
   if n = 0 then term else 
-    generate_bigger_inc ``BExp_BinExp BIExp_Plus (^term) (^term)`` (n-1)
+    generate_bigger_inc ``BExp_BinExp BIExp_Plus (^term) (^term)`` (n-1);
 
 fun power (x : int) (n : int) : int =
   if n = 0 then 1
   else 
     if (n mod 2) = 0 then 
       let val r = power x (n div 2) in r * r end
     else
-      let val r = power x (n div 2) in r * r * x end
+      let val r = power x (n div 2) in r * r * x end;
 
 
 
 fun benchmark () = 
 let
-  (* val n = power 2 4 ; *)
-  val n = 14 ;
-  val _ = print ("***** n : " ^ (Int.toString n) ^ " ***** \n") ;
-  val unamed_term = rhs (concl increment_exp_def) ;
+  (* val n = power 2 4; *)
+  val n = 14;
+  val _ = print ("***** n : " ^ (Int.toString n) ^ " ***** \n");
+  val unamed_term = rhs (concl increment_exp_def);
 
-  val _ = print "Generating term...\n" ;
-  val big_term = time (generate_bigger_inc unamed_term) n ;
-  val _ = print "Finished generating !\n" ;
+  val _ = print "Generating term...\n";
+  val big_term = time (generate_bigger_inc unamed_term) n;
+  val _ = print "Finished generating !\n";
 
-  val _ = print "Creating big_term definition...\n" ;
-  val exp_def = time (xDefine "big_term") `big_term = ^big_term` ;
-  val env = ``start_env 3w`` ;
+  val _ = print "Creating big_term definition...\n";
+  val exp_def = time (xDefine "big_term") `big_term = ^big_term`;
+  val env = ``start_env 3w``;
 
-  val _ = print "Starting measurements...\n" ;
-  val _ = print "EVAL measurement...\n" ;
-  val eval_value = time (compute_exp_EVAL ``big_term``) env ;
+  val _ = print "Starting measurements...\n";
+  val _ = print "EVAL measurement...\n";
+  val eval_value = time (compute_exp_EVAL ``big_term``) env;
 
-  val _ = print "cv measurement...\n" ;
-  val _ = translate_exp_cv exp_def ;
-  val cv_value = compute_exp_cv exp_def env ;
+  val _ = print "cv measurement...\n";
+  val _ = translate_exp_cv exp_def;
+  val cv_value = compute_exp_cv exp_def env;
 
   val _ = assert (fn x => (Term.compare (x, (rhs (concl cv_value))) = EQUAL)) (rhs (concl eval_value ))
 in 
   ()
-end
+end;
 
 
 

examples/compute/examples/increment/ex_incrementScript.sml

@@ -2,10 +2,10 @@
 (*  Example regarding a function that increments a variable in the env       *)
 (* ------------------------------------------------------------------------- *)
 
-open HolKernel Parse boolLib bossLib ;
-open bir_basicTheory bir_envTheory ;
-open bir_binexpTheory ;
-open bir_computeTheory ;
+open HolKernel Parse boolLib bossLib;
+open bir_basicTheory bir_envTheory;
+open bir_binexpTheory;
+open bir_computeTheory;
 
 
 val _ = new_theory "ex_increment";
@@ -42,4 +42,4 @@ QED
 
 
 
-val _ = export_theory () ;
+val _ = export_theory ();

examples/compute/examples/increment/test-increment.sml

@@ -1,3 +1,3 @@
-open ex_incrementLib ;
+open ex_incrementLib;
 
-val _ = benchmark () ;
+val _ = benchmark ();

examples/compute/examples/jump_chain/ex_jump_chainLib.sig

@@ -1,6 +1,6 @@
 signature ex_jump_chainLib = sig
 
-  val  benchmark_one_step : unit -> unit ;
+  val  benchmark_one_step : unit -> unit;
 
 
 end

examples/compute/examples/jump_chain/ex_jump_chainLib.sml

@@ -6,56 +6,57 @@
 structure ex_jump_chainLib :> ex_jump_chainLib =
 struct
 
-open HolKernel Parse bossLib boolLib ;
-open bir_programTheory bir_programSyntax ;
-open stringSyntax ;
-open bir_computeLib ;
+open HolKernel Parse bossLib boolLib;
+open bir_programTheory bir_programSyntax;
+open stringSyntax;
+open bir_computeLib;
 
 fun create_block (n : int) : term = 
-let val name = "block_" ^ (Int.toString n) ;
-  val label_name = stringSyntax.fromMLstring name ;
-  val next_name = "block_" ^ (Int.toString (n + 1)) ;
-  val next_label_name = fromMLstring next_name ;
-in ``<|bb_label := BL_Label (^label_name) ; bb_statements := [] ;
-  bb_last_statement := BStmt_Jmp (BLE_Label (BL_Label (^next_label_name)))|> `` end
+let val name = "block_" ^ (Int.toString n);
+  val label_name = stringSyntax.fromMLstring name;
+  val next_name = "block_" ^ (Int.toString (n + 1));
+  val next_label_name = fromMLstring next_name;
+in ``<|bb_label := BL_Label (^label_name); bb_statements := [];
+  bb_last_statement := BStmt_Jmp (BLE_Label (BL_Label (^next_label_name)))|> ``
+end;
 
 fun generate_big_program (n : int) = 
 let fun aux n k blist = if n = 0 then blist else aux (n-1) (k+1) ((create_block k)::blist)
-  val blist = rev $ aux n 0 [] ;
-  val blist_tm = listSyntax.mk_list (blist, ``:bir_block_t``) ;
-in bir_programSyntax.mk_program blist_tm end
+  val blist = rev $ aux n 0 [];
+  val blist_tm = listSyntax.mk_list (blist, ``:bir_block_t``);
+in bir_programSyntax.mk_program blist_tm end;
 
 
-val init_state_tm = ``<|bst_pc := <| bpc_label := BL_Label "block_0" ; 
-  bpc_index := 0 |> ; bst_environ := bir_empty_env ; bst_status := BST_Running |>`` ;
+val init_state_tm = ``<|bst_pc := <| bpc_label := BL_Label "block_0"; 
+  bpc_index := 0 |>; bst_environ := bir_empty_env; bst_status := BST_Running |>``;
 
 fun power (x : int) (n : int) : int =
   if n = 0 then 1
   else 
     if (n mod 2) = 0 then 
       let val r = power x (n div 2) in r * r end
     else
-      let val r = power x (n div 2) in r * r * x end
+      let val r = power x (n div 2) in r * r * x end;
 
 
 
 fun benchmark_one_step () =
 let
-  val n = power 2 10 ;
+  val n = power 2 10;
 
-  val program_tm = generate_big_program n ;
-  val program_def = Define `big_program = ^program_tm` ;
+  val program_tm = generate_big_program n;
+  val program_def = Define `big_program = ^program_tm`;
 
-  val _ = print "Starting measurements...\n" ;
-  val _ = print "EVAL measurement...\n" ;
-  val eval_value = time (compute_step_EVAL program_tm) init_state_tm ;
+  val _ = print "Starting measurements...\n";
+  val _ = print "EVAL measurement...\n";
+  val eval_value = time (compute_step_EVAL program_tm) init_state_tm;
 
-  val _ = print "cv measurement...\n" ;
-  val _ = print "Starting cv translation...\n" ;
-  val _ = time translate_program_cv program_def ;
-  val cv_value = compute_step_cv program_def init_state_tm ;
+  val _ = print "cv measurement...\n";
+  val _ = print "Starting cv translation...\n";
+  val _ = time translate_program_cv program_def;
+  val cv_value = compute_step_cv program_def init_state_tm;
 
   val _ = assert (fn x => (Term.compare (x, (rhs (concl cv_value))) = EQUAL)) (rhs (concl eval_value))
-in () end
+in () end;
 
 end

examples/compute/examples/jump_chain/test-jump-chain.sml

@@ -1,3 +1,3 @@
-open ex_jump_chainLib ;
+open ex_jump_chainLib;
 
-val _ = benchmark_one_step () ;
+val _ = benchmark_one_step ();

examples/compute/examples/mem_incr/ex_mem_incrLib.sig

@@ -1,9 +1,9 @@
 signature ex_mem_incrLib =
 sig
 
-  include Abbrev ;
+  include Abbrev;
 
-  val generate_bigger_inc : term -> int -> term ;
-  val benchmark : unit -> unit ;
+  val generate_bigger_inc : term -> int -> term;
+  val benchmark : unit -> unit;
 
 end

examples/compute/examples/mem_incr/ex_mem_incrLib.sml

@@ -6,11 +6,11 @@ structure ex_mem_incrLib :> ex_mem_incrLib =
 struct
 
 open HolKernel Parse bossLib boolLib;
-open bir_basicTheory ;
-open ex_mem_incrTheory ;
-open bir_computeLib ;
-open wordsTheory ;
-open numSyntax ;
+open bir_basicTheory;
+open ex_mem_incrTheory;
+open bir_computeLib;
+open wordsTheory;
+open numSyntax;
 
 
 fun generate_bigger_inc (term:term) (n:int) : term =
@@ -21,48 +21,48 @@ fun generate_bigger_inc (term:term) (n:int) : term =
       (BExp_BinExp BIExp_Plus 
         (BExp_Load (^term) (mem_addr (n2w ^(term_of_int n))) BEnd_BigEndian Bit8)
         (BExp_Load (^term) (mem_addr (n2w ^(term_of_int n))) BEnd_BigEndian Bit8))
-    `` (n-1)
+    `` (n-1);
 
 fun power (x : int) (n : int) : int =
   if n = 0 then 1
   else 
     if (n mod 2) = 0 then 
       let val r = power x (n div 2) in r * r end
     else
-      let val r = power x (n div 2) in r * r * x end
+      let val r = power x (n div 2) in r * r * x end;
 
 
 
 fun benchmark () = 
 let
-  (* val n = power 2 4 ; *)
-  val n = 12 ;
-  val n_tm = term_of_int n ;
-  val _ = print ("***** n : " ^ (Int.toString n) ^ " ***** \n") ;
-  val unamed_term = rhs (concl (SPEC ``(n2w ^n_tm):word64`` mem_incr_exp_def)) ;
-
-  val _ = print "Generating term...\n" ;
-  val big_term = time (generate_bigger_inc unamed_term) n ;
-  val _ = print "Finished generating !\n" ;
-  val _ = print "Cleaning the term by EVALing...\n" ;
-  val big_term_clean = rhs (concl (time EVAL big_term)) ;
-
-  val _ = print "Creating big_term definition...\n" ;
-  val exp_def = time (xDefine "big_term_clean") `big_term_clean = ^big_term_clean` ;
-  val env = ``start_env ^n_tm 5`` ;
-
-  val _ = print "Starting measurements...\n" ;
-  val _ = print "EVAL measurement...\n" ;
-  val eval_value = time (compute_exp_EVAL ``big_term_clean``) env ;
-
-  val _ = print "cv measurement...\n" ;
-  val _ = translate_exp_cv exp_def ;
-  val cv_value = compute_exp_cv exp_def env ;
+  (* val n = power 2 4; *)
+  val n = 12;
+  val n_tm = term_of_int n;
+  val _ = print ("***** n : " ^ (Int.toString n) ^ " ***** \n");
+  val unamed_term = rhs (concl (SPEC ``(n2w ^n_tm):word64`` mem_incr_exp_def));
+
+  val _ = print "Generating term...\n";
+  val big_term = time (generate_bigger_inc unamed_term) n;
+  val _ = print "Finished generating !\n";
+  val _ = print "Cleaning the term by EVALing...\n";
+  val big_term_clean = rhs (concl (time EVAL big_term));
+
+  val _ = print "Creating big_term definition...\n";
+  val exp_def = time (xDefine "big_term_clean") `big_term_clean = ^big_term_clean`;
+  val env = ``start_env ^n_tm 5``;
+
+  val _ = print "Starting measurements...\n";
+  val _ = print "EVAL measurement...\n";
+  val eval_value = time (compute_exp_EVAL ``big_term_clean``) env;
+
+  val _ = print "cv measurement...\n";
+  val _ = translate_exp_cv exp_def;
+  val cv_value = compute_exp_cv exp_def env;
 
   val _ = assert (fn x => (Term.compare (x, (rhs (concl cv_value))) = EQUAL)) (rhs (concl eval_value ))
 in 
   ()
-end
+end;
 
 
 

examples/compute/examples/mem_incr/ex_mem_incrScript.sml

@@ -3,14 +3,14 @@
 (* ------------------------------------------------------------------------- *)
 
 
-open HolKernel Parse bossLib boolLib ;
-open bir_basicTheory ;
-open bir_envTheory ;
-open finite_mapTheory ;
-open bir_computeTheory ;
+open HolKernel Parse bossLib boolLib;
+open bir_basicTheory;
+open bir_envTheory;
+open finite_mapTheory;
+open bir_computeTheory;
 
 
-val _ = new_theory "ex_mem_incr" ;
+val _ = new_theory "ex_mem_incr";
 
 Definition mem_var_def:
   mem_var = BVar "MEM8"
@@ -36,4 +36,4 @@ Definition mem_incr_exp_def:
 End
 
 
-val _ = export_theory () ;
+val _ = export_theory ();

examples/compute/examples/mem_incr/test-mem-incr.sml

@@ -1,3 +1,3 @@
-open ex_mem_incrLib ;
+open ex_mem_incrLib;
 
-val _ = benchmark () ;
+val _ = benchmark ();

examples/compute/examples/sum_list/ex_sum_listLib.sig

@@ -1,6 +1,6 @@
 signature ex_sum_listLib = sig
 
-  val  benchmark_one_step : unit -> unit ;
+  val  benchmark_one_step : unit -> unit;
 
 
 end