[interpretation] Some function renaming.

src/interpretation.ml

@@ -117,7 +117,7 @@ let const_real_of_float value =
 let value_term t = CRE.Value (Term t)
 let value_int i = CRE.Value (Int i)
 
-let builtin_caisar : caisar_env CRE.built_in_theories list =
+let caisar_builtins : caisar_env CRE.built_in_theories list =
   let reconstruct () =
     (* Force the engine to reconstruct the original term. *)
     raise Caml.Not_found
@@ -160,7 +160,7 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
     | [ Term _t1; Term _t2 ] -> reconstruct ()
     | _ -> invalid_arg (error_message ls)
   in
-  let length : _ CRE.builtin =
+  let vlength : _ CRE.builtin =
    fun engine ls vl _ty ->
     match vl with
     | [ Term { t_node = Tapp (ls, []); _ } ] -> (
@@ -214,10 +214,10 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
         let caisar_op = Vector (Language.create_vector env n) in
         value_term (term_of_caisar_op ~args engine caisar_op ty)
       | _ -> assert false)
-    | [ Term t1; Term t2 ] -> value_term (Term.t_app_infer ls [ t1; t2 ])
+    | [ Term _t1; Term _t2 ] -> reconstruct ()
     | _ -> invalid_arg (error_message ls)
   in
-  let mapi : _ CRE.builtin =
+  let vmapi : _ CRE.builtin =
    fun engine ls vl ty ->
     match vl with
     | [
@@ -302,8 +302,8 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
       [
         ([ Ident.op_get "" ] (* ([]) *), None, vget);
         ([ Ident.op_infix "-" ], None, vminus);
-        ([ "length" ], None, length);
-        ([ "mapi" ], None, mapi);
+        ([ "length" ], None, vlength);
+        ([ "mapi" ], None, vmapi);
       ] );
     ( [ "interpretation" ],
       "NeuralNetwork",
@@ -374,7 +374,7 @@ let interpret_task ~cwd env task =
     }
   in
   let engine =
-    CRE.create ~bounded_quant params env known_map caisar_env builtin_caisar
+    CRE.create ~bounded_quant params env known_map caisar_env caisar_builtins
   in
   let g, f = (Task.task_goal task, Task.task_goal_fmla task) in
   let f = CRE.normalize ~limit:Int.max_value engine Term.Mvs.empty f in