; Datatypes

(datatype expr 
    (Num i64)
    (Add expr expr)
    (Min expr expr expr))
(rewrite (Add (Num a) (Num b)) (Num (+ a b)))
(rewrite (Min (Num a) (Num b) (Num c)) (Num (min (min a b) c)))

; `String` supports limited operations, let's just use it as a char type
(datatype str
    (Cons String str))
(function EmptyConst () str)
(let Empty (EmptyConst))

; Length function

(function Length (str) expr)

(rule ((= f (Length Empty)))
      ((union (Length Empty) (Num 0))))

(rule ((= f (Length (Cons c cs))))
      ((union (Length (Cons c cs)) (Add (Num 1) (Length cs)))))

; EditDist function

(function EditDist (str str) expr)

(rule ((= f (EditDist Empty s)))
      ((union (EditDist Empty s) (Length s))))

(rule ((= f (EditDist s Empty)))
      ((union (EditDist s Empty) (Length s))))

(rule ((= f (EditDist (Cons head rest1) (Cons head rest2))))
      ((union (EditDist (Cons head rest1) (Cons head rest2))
            (EditDist rest1 rest2))))

(rule ((= f (EditDist (Cons head1 rest1) (Cons head2 rest2))) (!= head1 head2))
      ((union (EditDist (Cons head1 rest1) (Cons head2 rest2))
            (Add (Num 1)
                 (Min (EditDist rest1 rest2)
                      (EditDist (Cons head1 rest1) rest2)
                      (EditDist rest1 (Cons head2 rest2)))))))

; Unwrap function - turn a (Num n) into n

(function Unwrap (expr) i64)
(rule ((= x (Num n))) ((set (Unwrap (Num n)) n)))

; Tests
(let HorseStr (Cons "h" (Cons "o" (Cons "r" (Cons "s" (Cons "e" Empty))))))
(let RosStr (Cons "r" (Cons "o" (Cons "s" Empty))))
(let IntentionStr (Cons "i" (Cons "n" (Cons "t" (Cons "e" (Cons "n" (Cons "t" (Cons "i" (Cons "o" (Cons "n" Empty))))))))))
(let ExecutionStr (Cons "e" (Cons "x" (Cons "e" (Cons "c" (Cons "u" (Cons "t" (Cons "i" (Cons "o" (Cons "n" Empty))))))))))

(let Test1 (EditDist HorseStr RosStr))
(let Test2 (EditDist IntentionStr ExecutionStr))
(let Test3 (EditDist HorseStr Empty))

(run 100)

(extract (Unwrap Test1))
(check (= Test1 (Num 3)))

(extract (Unwrap Test2))
(check (= Test2 (Num 5)))

(extract (Unwrap Test3))
(check (= Test3 (Num 5)))