У меня есть следующий фрагмент кода Изабель:
type_synonym vname = string
datatype aexp = N int | V vname | Plus aexp aexp
fun full_plus :: "aexp ⇒ aexp ⇒ aexp" where
"full_plus (N n⇩1) (N n⇩2) = N (n⇩1+n⇩2)" |
"full_plus (N n⇩1) (Plus (N n⇩2) a) = (Plus (N (n⇩1+n⇩2)) a)" |
"full_plus (N n⇩1) (Plus a (N n⇩2)) = (Plus (N (n⇩1+n⇩2)) a)" |
"full_plus (Plus (N n⇩1) a) (N n⇩2) = (Plus (N (n⇩1+n⇩2)) a)" |
"full_plus (Plus a (N n⇩1)) (N n⇩2) = (Plus (N (n⇩1+n⇩2)) a)" |
"full_plus (Plus a⇩1 (N n⇩1)) (Plus a⇩2 (N n⇩2)) = (Plus (N (n⇩1+n⇩2)) (Plus a⇩1 a⇩2))" |
"full_plus (Plus a⇩1 (N n⇩1)) (Plus (N n⇩2) a⇩2) = (Plus (N (n⇩1+n⇩2)) (Plus a⇩1 a⇩2))" |
"full_plus (Plus (N n⇩1) a⇩1) (Plus a⇩2 (N n⇩2)) = (Plus (N (n⇩1+n⇩2)) (Plus a⇩1 a⇩2))" |
"full_plus (Plus (N n⇩1) a⇩1) (Plus (N n⇩2) a⇩2) = (Plus (N (n⇩1+n⇩2)) (Plus a⇩1 a⇩2))" |
"full_plus a⇩1 a⇩2 = Plus a⇩1 a⇩2"
Однако определение функции становится фиолетовым в jEdit.Я видел, как это происходит, когда я отмечаю рекурсивную лемму как [simp], поэтому я предполагаю, что это означает, что бэкэнд зависает или попадает в бесконечный цикл, но никогда с функциями.Мне кажется, что full_plus не рекурсивно ...?Я добавил declare [[simp_trace]] в программу, но это просто приводит к длинному и (для меня новичку) неразборчивому следу.Я могу опубликовать его здесь, если кто-то захочет его увидеть, но он довольно длинный.
Для справки, это упражнение 3.2 из бесплатной онлайн-книги по конкретной семантике.Надеюсь, кто-нибудь может мне помочь!