Pretend we use bigints for Sexp integers

* btl/builtins.typer: Slight reorganisation.
(Float->string): Rename from Float_to_string.
(Int->Integer): Give it a type.
(Sexp_integer): Change its type to be `Integer`.
(Sexp_dispatch): Make matching change.

* src/eval.ml: Add new "Int->Integer" primitive.
(make_integer): Make it take a bigint.
(sexp_dispatch): Make it use a bigint for the integer case.

btl/builtins.typer

@@ -86,32 +86,27 @@ Eq_comm p = Eq_cast (f := lambda xy -> Eq (t := t) xy x)
 Y = Built-in "Y" ((a : Type) ≡> (b : Type) ≡> (witness : a -> b) ≡>
                   ((a -> b) -> (a -> b)) -> (a -> b));
 
+Bool = typecons (Bool) (true) (false);
+true = datacons Bool true;
+false = datacons Bool false;
+
 %% Basic operators
 _+_ = Built-in "Int.+" (Int -> Int -> Int);
 _-_ = Built-in "Int.-" (Int -> Int -> Int);
 _*_ = Built-in "Int.*" (Int -> Int -> Int);
 _/_ = Built-in "Int./" (Int -> Int -> Int);
 
-Integer_+ = Built-in "Integer.+" (Integer -> Integer -> Integer);
-Integer_- = Built-in "Integer.-" (Integer -> Integer -> Integer);
-Integer_* = Built-in "Integer.*" (Integer -> Integer -> Integer);
-Integer_/ = Built-in "Integer./" (Integer -> Integer -> Integer);
-
-Float_+ = Built-in "Float.+" (Float -> Float -> Float);
-Float_- = Built-in "Float.-" (Float -> Float -> Float);
-Float_* = Built-in "Float.*" (Float -> Float -> Float);
-Float_/ = Built-in "Float./" (Float -> Float -> Float);
-Float_to_string = Built-in "Float.to_string" (Float -> String);
-
-Bool = typecons (Bool) (true) (false);
-true = datacons Bool true;
-false = datacons Bool false;
-
 Int_< = Built-in "Int.<" (Int -> Int -> Bool);
 Int_> = Built-in "Int.>" (Int -> Int -> Bool);
 Int_eq = Built-in "Int.=" (Int -> Int -> Bool);
 Int_<= = Built-in "Int.<=" (Int -> Int -> Bool);
 Int_>= = Built-in "Int.>=" (Int -> Int -> Bool);
+Int->Integer = Built-in "Int->Integer" (Int -> Integer);
+
+Integer_+ = Built-in "Integer.+" (Integer -> Integer -> Integer);
+Integer_- = Built-in "Integer.-" (Integer -> Integer -> Integer);
+Integer_* = Built-in "Integer.*" (Integer -> Integer -> Integer);
+Integer_/ = Built-in "Integer./" (Integer -> Integer -> Integer);
 
 Integer_< =  Built-in "Integer.<"  (Integer -> Integer -> Bool);
 Integer_> =  Built-in "Integer.>"  (Integer -> Integer -> Bool);
@@ -119,6 +114,12 @@ Integer_eq = Built-in "Integer.="  (Integer -> Integer -> Bool);
 Integer_<= = Built-in "Integer.<=" (Integer -> Integer -> Bool);
 Integer_>= = Built-in "Integer.>=" (Integer -> Integer -> Bool);
 
+Float_+ = Built-in "Float.+" (Float -> Float -> Float);
+Float_- = Built-in "Float.-" (Float -> Float -> Float);
+Float_* = Built-in "Float.*" (Float -> Float -> Float);
+Float_/ = Built-in "Float./" (Float -> Float -> Float);
+Float->String = Built-in "Float->String" (Float -> String);
+
 String_eq = Built-in "String.=" (String -> String -> Bool);
 Sexp_eq   = Built-in   "Sexp.=" (Sexp -> Sexp -> Bool);
 
@@ -127,9 +128,6 @@ Sexp_eq   = Built-in   "Sexp.=" (Sexp -> Sexp -> Bool);
 %% -----------------------------------------------------
 
 %% FIXME: "List : ?" should be sufficient but triggers
-%%   [!] Error     ELAB     `(List[2] a[1]) : ?ta · Id[18]` is not a proper type
-%%        > Call: (List[2] a[1])
-%%   "Subst-inversion-bug: <anon> · (↑2 () · () · () · Id)   ∘   <anon0> · () · (↑4 Id)    ==   <anon> · () · (↑2 Id)  !!"
 List : Type -> Type;
 %% List a = typecons List (nil) (cons a (List a));
 %% nil = lambda a ≡> datacons (List a) nil;
@@ -144,7 +142,7 @@ cons = datacons List cons;
 Sexp_symbol  = Built-in "Sexp.symbol"  (String    -> Sexp);
 Sexp_string  = Built-in "Sexp.string"  (String    -> Sexp);
 Sexp_node    = Built-in "Sexp.node"    (Sexp -> List Sexp -> Sexp);
-Sexp_integer = Built-in "Sexp.integer" (Int       -> Sexp);
+Sexp_integer = Built-in "Sexp.integer" (Integer   -> Sexp);
 Sexp_float   = Built-in "Sexp.float"   (Float     -> Sexp);
 
 Macro = typecons (Macro)
@@ -161,7 +159,7 @@ Sexp_dispatch = Built-in "Sexp.dispatch" (
                     -> (node   : Sexp -> List Sexp -> a)
                     -> (symbol : String -> a)
                     -> (string : String -> a)
-                    -> (int    : Int -> a)
+                    -> (int    : Integer -> a)
                     -> (float  : Float -> a)
                     -> (block  : List Sexp -> a)
                     -> a

src/eval.ml

@@ -147,7 +147,7 @@ let add_binary_bool_iop name f =
   let name = "Int." ^ name in
   let f loc (depth : eval_debug_info) (args_val: value_type list) =
     match args_val with
-    | [Vint (v); Vint (w)] -> o2v_bool (f v w)
+    | [Vint v; Vint w] -> o2v_bool (f v w)
     | _ -> error loc ("`" ^ name ^ "` expects 2 Int arguments") in
   add_builtin_function name f 2
 
@@ -157,11 +157,13 @@ let _ = add_binary_bool_iop "<"  (<);
         add_binary_bool_iop ">="  (>=);
         add_binary_bool_iop "<="  (<=)
 
+(* True integers (aka Z).  *)
+
 let add_binary_biop name f =
   let name = "Integer." ^ name in
   let f loc (depth : eval_debug_info) (args_val: value_type list) =
     match args_val with
-    | [Vinteger (v); Vinteger (w)] -> Vinteger (f v w)
+    | [Vinteger v; Vinteger w] -> Vinteger (f v w)
     | _ -> error loc ("`" ^ name ^ "` expects 2 Integer arguments") in
   add_builtin_function name f 2
 
@@ -174,7 +176,7 @@ let add_binary_bool_biop name f =
   let name = "Integer." ^ name in
   let f loc (depth : eval_debug_info) (args_val: value_type list) =
     match args_val with
-    | [Vinteger (v); Vinteger (w)] -> o2v_bool (f v w)
+    | [Vinteger v; Vinteger w] -> o2v_bool (f v w)
     | _ -> error loc ("`" ^ name ^ "` expects 2 Integer arguments") in
   add_builtin_function name f 2
 
@@ -182,13 +184,23 @@ let _ = add_binary_bool_biop "<"  BI.lt_big_int;
         add_binary_bool_biop ">"  BI.gt_big_int;
         add_binary_bool_biop "="  BI.eq_big_int;
         add_binary_bool_biop ">=" BI.ge_big_int;
-        add_binary_bool_biop "<=" BI.le_big_int
+        add_binary_bool_biop "<=" BI.le_big_int;
+        let name = "Int->Integer" in
+        add_builtin_function
+          name
+          (fun loc (depth : eval_debug_info) (args_val: value_type list)
+           -> match args_val with
+             | [Vint v] -> Vinteger (BI.big_int_of_int v)
+             | _ -> error loc ("`" ^ name ^ "` expects 1 Int argument"))
+          1
+
+(* Floating point numers.  *)
 
 let add_binary_fop name f =
   let name = "Float." ^ name in
   let f loc (depth : eval_debug_info) (args_val: value_type list) =
     match args_val with
-    | [Vfloat (v); Vfloat (w)] -> Vfloat (f v w)
+    | [Vfloat v; Vfloat w] -> Vfloat (f v w)
     | _ -> error loc ("`" ^ name ^ "` expects 2 Float arguments") in
   add_builtin_function name f 2
 
@@ -221,10 +233,9 @@ let make_string loc depth args_val  = match args_val with
   | _ -> error loc "Sexp.string expects one string as argument"
 
 let make_integer loc depth args_val = match args_val with
-  | [Vint (str)] -> Vsexp (Integer (loc, str))
+  | [Vinteger n] -> Vsexp (Integer (loc, BI.int_of_big_int n))
   | _ -> error loc "Sexp.integer expects one integer as argument"
 
-
 let make_float loc depth args_val   = match args_val with
   | [Vfloat x] -> Vsexp (Float (loc, x))
   | _ -> error loc "Sexp.float expects one float as argument"
@@ -285,13 +296,13 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type
     match lxp with
         (*  Leafs           *)
         (* ---------------- *)
-        | Imm(Integer (_, i))       -> Vint (i)
-        | Imm(String (_, s))        -> Vstring (s)
-        | Imm(Float (_, n))         -> Vfloat (n)
-        | Imm(sxp)                  -> Vsexp (sxp)
+        | Imm(Integer (_, i))       -> Vint i
+        | Imm(String (_, s))        -> Vstring s
+        | Imm(Float (_, n))         -> Vfloat n
+        | Imm(sxp)                  -> Vsexp sxp
         | Cons (label)              -> Vcons (label, [])
         | Lambda ((_, n), lxp)      -> Closure (n, lxp, ctx)
-        | Builtin ((_, str))        -> Vbuiltin (str)
+        | Builtin ((_, str))        -> Vbuiltin str
 
         (* Return a value stored in env *)
         | Var((loc, name), idx) as e
@@ -490,16 +501,17 @@ and sexp_dispatch loc depth args =
 
         | Symbol  (_ , s)    ->
              let rctx = ctx_sym in
-             eval sym (add_rte_variable None (Vstring(s)) rctx)
+             eval sym (add_rte_variable None (Vstring s) rctx)
         | String  (_ , s)    ->
              let rctx = ctx_str in
-             eval str (add_rte_variable None (Vstring(s)) rctx)
+             eval str (add_rte_variable None (Vstring s) rctx)
         | Integer (_ , i)    ->
              let rctx = ctx_it in
-             eval it (add_rte_variable None (Vint(i)) rctx)
+             eval it (add_rte_variable None (Vinteger (BI.big_int_of_int i))
+                        rctx)
         | Float   (_ , f)    ->
              let rctx = ctx_flt in
-             eval flt (add_rte_variable None (Vfloat(f)) rctx) (*
+             eval flt (add_rte_variable None (Vfloat f) rctx) (*
         | Block   (_ , s, _) ->
              eval blk (add_rte_variable None (o2v_list s)) *)
         | _ ->
@@ -588,7 +600,7 @@ let io_return loc depth args_val = match args_val with
 
 let float_to_string loc depth args_val = match args_val with
   | [Vfloat x] -> Vstring (string_of_float x)
-  | _ -> error loc "Float.to_string expects one Float arg"
+  | _ -> error loc "Float->string expects one Float arg"
 
 let sys_exit loc depth args_val = match args_val with
   | [Vint n] -> Vcommand (fun _ -> exit n)
@@ -626,7 +638,7 @@ let register_builtin_functions () =
               ("Sexp.dispatch" , sexp_dispatch, 7);
               ("String.="      , string_eq, 2);
               ("Sexp.="        , sexp_eq, 2);
-              ("Float.to_string", float_to_string, 1);
+              ("Float->String", float_to_string, 1);
               ("IO.bind"       , io_bind, 2);
               ("IO.return"     , io_return, 1);
               ("IO.run"        , io_run, 2);

src/opslexp.ml

@@ -420,6 +420,7 @@ let rec check' erased ctx e =
                         -> (let _ = check_type DB.set_empty ctx t in
                            DB.lctx_extend ctx (Some v) ForwardRef t))
                        ctx defs in
+      (* FIXME: Allow erasable let-bindings!  *)
       let nerased = DB.set_sink (List.length defs) erased in
       let nctx = DB.lctx_extend_rec ctx defs in
       (* FIXME: Termination checking!  Positivity-checker!  *)

src/sexp.ml

@@ -33,6 +33,9 @@ type sexp =                  (* Syntactic expression, kind of like Lisp.  *)
   | Block of location * pretoken list * location
   | Symbol of symbol
   | String of location * string
+  (* FIXME: It would make a lof of sense to use a bigint here, but `compare`
+   * burps on Big_int objects, and `compare` is used for hash-consing of lexp
+   * objects which contain sexp objects as well.  *)
   | Integer of location * integer
   | Float of location * float
   | Node of sexp * sexp list

tests/eval_test.ml

@@ -343,7 +343,7 @@ let _ = test_eval_eqv_named
   "Implicit Arguments"
 
   "default = new-attribute Macro;
-   default = add-attribute default Int (macro (lambda (lst : List Sexp) -> Sexp_integer 1));
+   default = add-attribute default Int (macro (lambda (lst : List Sexp) -> Sexp_integer (Int->Integer 1)));
 
    fun = lambda (x : Int) =>
       lambda (y : Int) ->

tests/macro_test.ml

@@ -75,7 +75,7 @@ let _ = (add_test "MACROS" "macros decls" (fun () ->
 
         let make-decl : String -> Int -> Sexp;
             make-decl name val =
-          (Sexp_node (Sexp_symbol \"_=_\") (cons (Sexp_symbol name) (cons (Sexp_integer val) nil))) in
+          (Sexp_node (Sexp_symbol \"_=_\") (cons (Sexp_symbol name) (cons (Sexp_integer (Int->Integer val)) nil))) in
 
         let d1 = make-decl \"a\" 1 in
         let d2 = make-decl \"b\" 2 in