Stefan pushed to branch master at Stefan / Typer
Commits: 098ca889 by Stefan Monnier at 2017-09-26T02:15:31Z 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.
- - - - -
6 changed files:
- btl/builtins.typer - src/eval.ml - src/opslexp.ml - src/sexp.ml - tests/eval_test.ml - tests/macro_test.ml
Changes:
===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/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 ===================================== --- a/src/eval.ml +++ b/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 ===================================== --- a/src/opslexp.ml +++ b/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 ===================================== --- a/src/sexp.ml +++ b/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 ===================================== --- a/tests/eval_test.ml +++ b/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 ===================================== --- a/tests/macro_test.ml +++ b/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
View it on GitLab: https://gitlab.com/monnier/typer/commit/098ca889df9159b692dc6f8896ffb59588e6...
--- View it on GitLab: https://gitlab.com/monnier/typer/commit/098ca889df9159b692dc6f8896ffb59588e6... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date