SMLで証明されたマージソートを使う

mergesort.sml

(** val app : 'a1 list -> 'a1 list -> 'a1 list **)

val app = (fn x => fn y => x @ y)

signature TotalLeBool' = 
 sig 
  type t 
  
  val leb : t -> t -> bool
 end

functor Sort
  (X:TotalLeBool')  = 
 struct 
  (** val merge : X.t list -> X.t list -> X.t list **)
  
  fun merge l1 l2 =
    let fun merge_aux l3 =
      case l1 of
        [] => l3
      | a1::l1' =>
        (case l3 of
           [] => l1
         | a2::l2' =>
           if X.leb a1 a2 then a1::(merge l1' l3) else a2::(merge_aux l2'))
    in merge_aux l2 end 
  
  (** val merge_list_to_stack :
      X.t list option list -> X.t list -> X.t list option list **)
  
  fun merge_list_to_stack stack l =
    case stack of
      [] => (SOME l)::[]
    | y::stack' =>
      (case y of
         SOME l' => NONE::(merge_list_to_stack stack' (merge l' l))
       | NONE => (SOME l)::stack')
  
  (** val merge_stack : X.t list option list -> X.t list **)
  
  fun merge_stack stack =
    case stack of
      [] => []
    | y::stack' =>
      (case y of
         SOME l => merge l (merge_stack stack')
       | NONE => merge_stack stack')
  
  (** val iter_merge : X.t list option list -> X.t list -> X.t list **)
  
  fun iter_merge stack l =
    case l of
      [] => merge_stack stack
    | a::l' => iter_merge (merge_list_to_stack stack (a::[])) l'
  
  (** val sort : X.t list -> X.t list **)
  
  val sort =
    iter_merge []
  
  (** val flatten_stack : X.t list option list -> X.t list **)
  
  fun flatten_stack stack =
    case stack of
      [] => []
    | o0::stack' =>
      (case o0 of
         SOME l => app l (flatten_stack stack')
       | NONE => flatten_stack stack')
 end

mergesort.v

Require Import Mergesort.
Extraction Language Sml.
Extract Constant app => "(fn x => fn y => x @ y)". 
Extract Inductive option => "option" ["SOME" "NONE"].
Extract Inductive bool => bool ["true" "false"].
Extract Inductive list => "list" ["[]" "(::)"].
Extraction "mergesort.sml" Sort.