Update translation of annotations to Lean and Coq

julianmendez · Jan 30, 2024 · 74cd8e0 · 74cd8e0
1 parent 827dc6b
commit 74cd8e0
Show file tree

Hide file tree

Showing 5 changed files with 43 additions and 31 deletions.
diff --git a/translator/src/main/scala/soda/translator/extension/tocoq/Package.scala b/translator/src/main/scala/soda/translator/extension/tocoq/Package.scala
@@ -1450,9 +1450,11 @@ trait TranslationConstantToCoq
       Tuple2 (soda_constant .or_reserved_word , coq_or_reserved_word) ,
       Tuple2 (soda_constant .equals_symbol , coq_equals_symbol) ,
       Tuple2 (soda_constant .less_than_symbol , coq_less_than_symbol) ,
-      Tuple2 (soda_constant .less_than_or_equal_to_symbol , coq_less_than_or_equal_to_symbol),
-      Tuple2 (soda_constant .less_than_or_equal_to_unicode_symbol ,
-        coq_less_than_or_equal_to_symbol)
+      Tuple2 (soda_constant .less_than_or_equal_to_symbol , coq_less_than_or_equal_to_symbol) ,
+      Tuple2 (soda_constant .tail_recursion_annotation , coq_empty_string) ,
+      Tuple2 (soda_constant .override_annotation , coq_empty_string) ,
+      Tuple2 (soda_constant .new_annotation , coq_empty_string)
+
     )
 
   lazy val type_translation : Seq [Tuple2 [String, String] ] =

diff --git a/translator/src/main/scala/soda/translator/extension/tocoq/TranslationConstantToCoq.soda b/translator/src/main/scala/soda/translator/extension/tocoq/TranslationConstantToCoq.soda
@@ -264,9 +264,11 @@ class TranslationConstantToCoq
       Tuple2 (soda_constant .or_reserved_word , coq_or_reserved_word) ,
       Tuple2 (soda_constant .equals_symbol , coq_equals_symbol) ,
       Tuple2 (soda_constant .less_than_symbol , coq_less_than_symbol) ,
-      Tuple2 (soda_constant .less_than_or_equal_to_symbol , coq_less_than_or_equal_to_symbol),
-      Tuple2 (soda_constant .less_than_or_equal_to_unicode_symbol ,
-        coq_less_than_or_equal_to_symbol)
+      Tuple2 (soda_constant .less_than_or_equal_to_symbol , coq_less_than_or_equal_to_symbol) ,
+      Tuple2 (soda_constant .tail_recursion_annotation , coq_empty_string) ,
+      Tuple2 (soda_constant .override_annotation , coq_empty_string) ,
+      Tuple2 (soda_constant .new_annotation , coq_empty_string)
+
     )
 
   type_translation : Seq [Tuple2 [String] [String] ] =

diff --git a/translator/src/main/scala/soda/translator/extension/tolean/Package.scala b/translator/src/main/scala/soda/translator/extension/tolean/Package.scala
@@ -1607,23 +1607,27 @@ trait TranslationConstantToLean
 
   lazy val type_symbols_translation : Seq [Tuple2 [String, String] ] =
     Seq (
-      Tuple2 (soda_constant .subtype_reserved_word , lean_subtype_symbol),
-      Tuple2 (soda_constant .supertype_reserved_word , lean_supertype_symbol),
-      Tuple2 (soda_constant .function_arrow_symbol , lean_function_arrow_symbol),
-      Tuple2 (soda_constant .opening_bracket_symbol, lean_opening_parenthesis + lean_space),
+      Tuple2 (soda_constant .subtype_reserved_word , lean_subtype_symbol) ,
+      Tuple2 (soda_constant .supertype_reserved_word , lean_supertype_symbol) ,
+      Tuple2 (soda_constant .function_arrow_symbol , lean_function_arrow_symbol) ,
+      Tuple2 (soda_constant .opening_bracket_symbol, lean_opening_parenthesis + lean_space) ,
       Tuple2 (soda_constant .closing_bracket_symbol , lean_space + lean_closing_parenthesis)
     )
 
   lazy val function_symbols_translation : Seq [Tuple2 [String, String] ] =
     Seq (
-      Tuple2 (soda_constant .function_definition_symbol , lean_function_definition_symbol),
-      Tuple2 (soda_constant .lambda_reserved_word , lean_fun_reserved_word),
-      Tuple2 (soda_constant .any_reserved_word , lean_fun_reserved_word),
-      Tuple2 (soda_constant .lambda_arrow_symbol , lean_lambda_arrow_symbol),
-      Tuple2 (soda_constant .case_arrow_symbol , lean_case_arrow_symbol),
-      Tuple2 (soda_constant .not_reserved_word , lean_not_reserved_word),
-      Tuple2 (soda_constant .and_reserved_word , lean_and_symbol),
-      Tuple2 (soda_constant .or_reserved_word , lean_or_symbol)
+      Tuple2 (soda_constant .function_definition_symbol , lean_function_definition_symbol) ,
+      Tuple2 (soda_constant .lambda_reserved_word , lean_fun_reserved_word) ,
+      Tuple2 (soda_constant .any_reserved_word , lean_fun_reserved_word) ,
+      Tuple2 (soda_constant .lambda_arrow_symbol , lean_lambda_arrow_symbol) ,
+      Tuple2 (soda_constant .case_arrow_symbol , lean_case_arrow_symbol) ,
+      Tuple2 (soda_constant .not_reserved_word , lean_not_reserved_word) ,
+      Tuple2 (soda_constant .and_reserved_word , lean_and_symbol) ,
+      Tuple2 (soda_constant .or_reserved_word , lean_or_symbol) ,
+      Tuple2 (soda_constant .tail_recursion_annotation , lean_empty_string) ,
+      Tuple2 (soda_constant .override_annotation , lean_empty_string) ,
+      Tuple2 (soda_constant .new_annotation , lean_empty_string)
+
     )
 
   lazy val type_translation : Seq [Tuple2 [String, String]  ] =

diff --git a/translator/src/main/scala/soda/translator/extension/tolean/TranslationConstantToLean.soda b/translator/src/main/scala/soda/translator/extension/tolean/TranslationConstantToLean.soda
@@ -437,23 +437,27 @@ class TranslationConstantToLean
 
   type_symbols_translation : Seq [Tuple2 [String] [String] ] =
     Seq (
-      Tuple2 (soda_constant .subtype_reserved_word , lean_subtype_symbol),
-      Tuple2 (soda_constant .supertype_reserved_word , lean_supertype_symbol),
-      Tuple2 (soda_constant .function_arrow_symbol , lean_function_arrow_symbol),
-      Tuple2 (soda_constant .opening_bracket_symbol, lean_opening_parenthesis + lean_space),
+      Tuple2 (soda_constant .subtype_reserved_word , lean_subtype_symbol) ,
+      Tuple2 (soda_constant .supertype_reserved_word , lean_supertype_symbol) ,
+      Tuple2 (soda_constant .function_arrow_symbol , lean_function_arrow_symbol) ,
+      Tuple2 (soda_constant .opening_bracket_symbol, lean_opening_parenthesis + lean_space) ,
       Tuple2 (soda_constant .closing_bracket_symbol , lean_space + lean_closing_parenthesis)
     )
 
   function_symbols_translation : Seq [Tuple2 [String] [String] ] =
     Seq (
-      Tuple2 (soda_constant .function_definition_symbol , lean_function_definition_symbol),
-      Tuple2 (soda_constant .lambda_reserved_word , lean_fun_reserved_word),
-      Tuple2 (soda_constant .any_reserved_word , lean_fun_reserved_word),
-      Tuple2 (soda_constant .lambda_arrow_symbol , lean_lambda_arrow_symbol),
-      Tuple2 (soda_constant .case_arrow_symbol , lean_case_arrow_symbol),
-      Tuple2 (soda_constant .not_reserved_word , lean_not_reserved_word),
-      Tuple2 (soda_constant .and_reserved_word , lean_and_symbol),
-      Tuple2 (soda_constant .or_reserved_word , lean_or_symbol)
+      Tuple2 (soda_constant .function_definition_symbol , lean_function_definition_symbol) ,
+      Tuple2 (soda_constant .lambda_reserved_word , lean_fun_reserved_word) ,
+      Tuple2 (soda_constant .any_reserved_word , lean_fun_reserved_word) ,
+      Tuple2 (soda_constant .lambda_arrow_symbol , lean_lambda_arrow_symbol) ,
+      Tuple2 (soda_constant .case_arrow_symbol , lean_case_arrow_symbol) ,
+      Tuple2 (soda_constant .not_reserved_word , lean_not_reserved_word) ,
+      Tuple2 (soda_constant .and_reserved_word , lean_and_symbol) ,
+      Tuple2 (soda_constant .or_reserved_word , lean_or_symbol) ,
+      Tuple2 (soda_constant .tail_recursion_annotation , lean_empty_string) ,
+      Tuple2 (soda_constant .override_annotation , lean_empty_string) ,
+      Tuple2 (soda_constant .new_annotation , lean_empty_string)
+
     )
 
   type_translation : Seq [Tuple2 [String] [String]  ] =

diff --git a/...or/src/test/resources/soda/translator/example/forcoq/mathematics/TriangularNumberForCoq.v b/...or/src/test/resources/soda/translator/example/forcoq/mathematics/TriangularNumberForCoq.v
@@ -8,7 +8,7 @@ Class TriangularNumberForCoq : Type :=
 
 Notation "'TriangularNumberForCoq_'" := TriangularNumberForCoq.mk (at level 99) .
 
-Fixpoint   @tailrec
+Fixpoint   
    _tailrec_get_number (m : nat) (acc : nat) : nat :=
     match m with
       | S_ (k) => _tailrec_get_number (k) (acc .(add) (S_ (k) ) )