Stefan pushed to branch master at Stefan / Typer

Commits: 9ae0cbe3 by Stefan Monnier at 2017-09-25T15:30:10Z Add preliminary support for big-ints

* GNUmakefile (OBFLAGS): Add `nums`. * src/debruijn.ml (type_integer): New type. * src/builtin.ml (register_builtin_csts): Register it. * src/env.ml (value_type): Add big-int constructor. * src/eval.ml (add_binary_biop, add_binary_bool_biop): New functions. Use them to setup new primitives. * btl/builtins.typer (Integer_*): Give them types.

- - - - -

6 changed files:

- GNUmakefile - btl/builtins.typer - src/builtin.ml - src/debruijn.ml - src/env.ml - src/eval.ml

Changes:

===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -8,7 +8,7 @@ SRC_FILES := $(wildcard ./src/*.ml) CPL_FILES := $(wildcard ./$(BUILDDIR)/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml)

-OBFLAGS = -tag debug -tag profile -build-dir $(BUILDDIR) +OBFLAGS = -tag debug -tag profile -lib nums -build-dir $(BUILDDIR) # OBFLAGS := -I $(SRCDIR) -build-dir $(BUILDDIR) -pkg str # OBFLAGS_DEBUG := -tag debug -tag profile -tag "warn(+20)" # OBFLAGS_RELEASE := -tag unsafe -tag inline

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -59,7 +59,7 @@ Eq_comm p = Eq_cast (f := lambda xy -> Eq (t := t) xy x) Eq_refl;

%% General recursion!! -%% Whether this breaks onsistency or not is a good question. +%% Whether this breaks consistency or not is a good question. %% The basic idea is the following: %% %% The `witness` argument presumably makes sure that "Y f" can only @@ -92,6 +92,11 @@ _-_ = 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); @@ -108,6 +113,12 @@ Int_eq = Built-in "Int.=" (Int -> Int -> Bool); Int_<= = Built-in "Int.<=" (Int -> Int -> Bool); Int_>= = Built-in "Int.>=" (Int -> Int -> Bool);

+Integer_< = Built-in "Integer.<" (Integer -> Integer -> Bool); +Integer_> = Built-in "Integer.>" (Integer -> Integer -> Bool); +Integer_eq = Built-in "Integer.=" (Integer -> Integer -> Bool); +Integer_<= = Built-in "Integer.<=" (Integer -> Integer -> Bool); +Integer_>= = Built-in "Integer.>=" (Integer -> Integer -> Bool); + String_eq = Built-in "String.=" (String -> String -> Bool); Sexp_eq = Built-in "Sexp.=" (Sexp -> Sexp -> Bool);

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -154,6 +154,7 @@ let register_builtin_csts () = add_builtin_cst "Type" DB.type0; add_builtin_cst "Type1" DB.type1; add_builtin_cst "Int" DB.type_int; + add_builtin_cst "Integer" DB.type_integer; add_builtin_cst "Float" DB.type_float; add_builtin_cst "String" DB.type_string

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -89,6 +89,7 @@ let type0 = mkSort (dloc, Stype level0) let type1 = mkSort (dloc, Stype level1) let type2 = mkSort (dloc, Stype level2) let type_int = mkBuiltin ((dloc, "Int"), type0, None) +let type_integer = mkBuiltin ((dloc, "Integer"), type0, None) let type_float = mkBuiltin ((dloc, "Float"), type0, None) let type_string = mkBuiltin ((dloc, "String"), type0, None)

===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -38,6 +38,7 @@ open Sexp open Elexp module M = Myers module L = Lexp +module BI = Big_int

let dloc = dummy_location

@@ -48,6 +49,7 @@ let str_idx idx = "[" ^ (string_of_int idx) ^ "]"

type value_type = | Vint of int + | Vinteger of BI.big_int | Vstring of string | Vcons of symbol * value_type list | Vbuiltin of string @@ -67,6 +69,7 @@ type value_type = let rec value_equal a b = match a, b with | Vint (i1), Vint (i2) -> i1 = i2 + | Vinteger (i1), Vinteger (i2) -> BI.eq_big_int i1 i2 | Vstring (s1), Vstring (s2) -> s1 = s2 | Vbuiltin (s1), Vbuiltin (s2) -> s1 = s2 | Vfloat (f1), Vfloat (f2) -> f1 = f2 @@ -107,6 +110,7 @@ let value_name v = | Vin _ -> "Vin" | Vout _ -> "Vout" | Vint _ -> "Vint" + | Vinteger _ -> "Vinteger" | Vsexp _ -> "Vsexp" | Vtype _ -> "Vtype" | Vcons _ -> "Vcons"

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -157,6 +157,33 @@ let _ = add_binary_bool_iop "<" (<); add_binary_bool_iop ">=" (>=); add_binary_bool_iop "<=" (<=)

+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) + | _ -> error loc ("`" ^ name ^ "` expects 2 Integer arguments") in + add_builtin_function name f 2 + +let _ = add_binary_biop "+" BI.add_big_int; + add_binary_biop "-" BI.sub_big_int; + add_binary_biop "*" BI.mult_big_int; + add_binary_biop "/" BI.div_big_int + +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) + | _ -> error loc ("`" ^ name ^ "` expects 2 Integer arguments") in + add_builtin_function name f 2 + +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 + let add_binary_fop name f = let name = "Float." ^ name in let f loc (depth : eval_debug_info) (args_val: value_type list) =

View it on GitLab: https://gitlab.com/monnier/typer/commit/9ae0cbe3c74ea3a1965ba2cd48a076fb4e9c...

--- View it on GitLab: https://gitlab.com/monnier/typer/commit/9ae0cbe3c74ea3a1965ba2cd48a076fb4e9c... You're receiving this email because of your account on gitlab.com.