Skip to content

Commit

Permalink
Syntax factory (#1530)
Browse files Browse the repository at this point in the history
  • Loading branch information
@cyrus-
cyrus- authored Mar 4, 2025
2 parents 4390190 + 9d3f368 commit 6df1774
Show file tree
Hide file tree
Showing 17 changed files with 2,212 additions and 1,978 deletions.
224 changes: 111 additions & 113 deletions src/haz3lcore/dynamics/Builtins.re
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
open Util;
open OptUtil.Syntax;
open DHExp;

/*
Built-in functions for Hazel.
Expand All @@ -10,6 +9,7 @@ open DHExp;
See the existing ones for reference.
*/
module Fresh = IdTagged.FreshGrammar;

[@deriving (show({with_path: false}), sexp)]
type builtin =
Expand Down Expand Up @@ -47,14 +47,15 @@ let (let-unbox) = ((request, v), f) =>

module Pervasives = {
module Impls = {
open Fresh.Exp;
/* constants */
let infinity = Float(Float.infinity) |> fresh;
let neg_infinity = Float(Float.neg_infinity) |> fresh;
let nan = Float(Float.nan) |> fresh;
let epsilon_float = Float(epsilon_float) |> fresh;
let pi = Float(Float.pi) |> fresh;
let max_int = Int(Int.max_int) |> fresh;
let min_int = Int(Int.min_int) |> fresh;
let infinity = float(Float.infinity);
let neg_infinity = float(Float.neg_infinity);
let nan = float(Float.nan);
let epsilon_float = float(epsilon_float);
let pi = float(Float.pi);
let max_int = int(Int.max_int);
let min_int = int(Int.min_int);

[@warning "-8"]
// let-unbox guarantees that the tuple will have length 2
Expand All @@ -73,52 +74,52 @@ module Pervasives = {

let is_finite = d => {
let-unbox f = (Float, d);
Some(fresh(Bool(Float.is_finite(f))));
Some(bool(Float.is_finite(f)));
};

let is_infinite = d => {
let-unbox f = (Float, d);
Some(fresh(Bool(Float.is_infinite(f))));
Some(bool(Float.is_infinite(f)));
};

let is_nan = d => {
let-unbox f = (Float, d);
Some(fresh(Bool(Float.is_nan(f))));
Some(bool(Float.is_nan(f)));
};

let string_of_int = d => {
let-unbox n = (Int, d);
Some(fresh(String(string_of_int(n))));
Some(string(string_of_int(n)));
};

let string_of_float = d => {
let-unbox f = (Float, d);
Some(fresh(String(string_of_float(f))));
Some(string(string_of_float(f)));
};

let string_of_bool = d => {
let-unbox b = (Bool, d);
Some(fresh(String(string_of_bool(b))));
Some(string(string_of_bool(b)));
};

let int_of_float = d => {
let-unbox f = (Float, d);
Some(fresh(Int(int_of_float(f))));
Some(int(int_of_float(f)));
};

let float_of_int = d => {
let-unbox n = (Int, d);
Some(fresh(Float(float_of_int(n))));
Some(float(float_of_int(n)));
};

let abs = d => {
let-unbox n = (Int, d);
Some(fresh(Int(abs(n))));
Some(int(abs(n)));
};

let float_op = (fn, d) => {
let-unbox f = (Float, d);
Some(fresh(Float(fn(f))));
Some(float(fn(f)));
};

let abs_float = float_op(abs_float);
Expand Down Expand Up @@ -146,53 +147,48 @@ module Pervasives = {
switch (convert(s)) {
| Some(n) => Some(wrap(n))
| None =>
let d' = BuiltinFun(name) |> DHExp.fresh;
let d' = Ap(Forward, d', d) |> DHExp.fresh;
let d' = DynamicErrorHole(d', InvalidOfString) |> DHExp.fresh;
let d' = builtin_fun(name);
let d' = ap(Forward, d', d);
let d' = dynamic_error_hole(d', InvalidOfString);
Some(d');
};
};

let int_of_string =
of_string(int_of_string_opt, n => Int(n) |> DHExp.fresh);
let float_of_string =
of_string(float_of_string_opt, f => Float(f) |> DHExp.fresh);
let bool_of_string =
of_string(bool_of_string_opt, b => Bool(b) |> DHExp.fresh);
let int_of_string = of_string(int_of_string_opt, n => int(n));
let float_of_string = of_string(float_of_string_opt, f => float(f));
let bool_of_string = of_string(bool_of_string_opt, b => bool(b));

let int_mod = name =>
binary((d1, d2) => {
let-unbox m = (Int, d1);
let-unbox n = (Int, d2);
if (n == 0) {
Some(
fresh(
DynamicErrorHole(
Ap(Forward, BuiltinFun(name) |> fresh, d1) |> fresh,
DivideByZero,
),
dynamic_error_hole(
ap(Forward, builtin_fun(name), d1),
DivideByZero,
),
);
} else {
Some(fresh(Int(m mod n)));
Some(int(m mod n));
};
});

let string_length = d => {
let-unbox s = (String, d);
Some(fresh(Int(String.length(s))));
Some(int(String.length(s)));
};

let string_compare =
binary((d1, d2) => {
let-unbox s1 = (String, d1);
let-unbox s2 = (String, d2);
Some(fresh(Int(String.compare(s1, s2))));
Some(int(String.compare(s1, s2)));
});

let string_trim = d => {
let-unbox s = (String, d);
Some(fresh(String(String.trim(s))));
Some(string(String.trim(s)));
};

let string_of: DHExp.t => option(string) =
Expand All @@ -206,15 +202,15 @@ module Pervasives = {
let-unbox s1 = (String, d1);
let-unbox xs = (List, d2);
let* xs' = List.map(string_of, xs) |> Util.OptUtil.sequence;
Some(fresh(String(String.concat(s1, xs'))));
Some(string(String.concat(s1, xs')));
});

let string_sub = name =>
ternary((d1, d2, d3) => {
let-unbox s = (String, d1);
let-unbox idx = (Int, d2);
let-unbox len = (Int, d3);
try(Some(fresh(String(String.sub(s, idx, len))))) {
try(Some(string(String.sub(s, idx, len)))) {
| _ =>
let d' = BuiltinFun(name) |> DHExp.fresh;
let d' = Ap(Forward, d', d1) |> DHExp.fresh;
Expand All @@ -228,85 +224,87 @@ module Pervasives = {
let-unbox s = (String, d1);
let-unbox sep = (String, d2);
let split_str = Util.StringUtil.plain_split(sep, s);
let split_str' = List.map(s => String(s) |> DHExp.fresh, split_str);
Some(fresh(ListLit(split_str')));
let split_str' = List.map(s => string(s), split_str);
Some(list_lit(split_str'));
});
};

open Impls;

// Update src/haz3lmenhir/Lexer.mll when any new builtin is added
let builtins =
VarMap.empty
|> const("infinity", Float, infinity)
|> const("neg_infinity", Float, neg_infinity)
|> const("nan", Float, nan)
|> const("epsilon_float", Float, epsilon_float)
|> const("pi", Float, pi)
|> const("max_int", Int, max_int)
|> const("min_int", Int, min_int)
|> fn("is_finite", Float, Bool, is_finite)
|> fn("is_infinite", Float, Bool, is_infinite)
|> fn("is_nan", Float, Bool, is_nan)
|> fn("int_of_float", Float, Int, int_of_float)
|> fn("float_of_int", Int, Float, float_of_int)
|> fn("string_of_int", Int, String, string_of_int)
|> fn("string_of_float", Float, String, string_of_float)
|> fn("string_of_bool", Bool, String, string_of_bool)
|> fn("int_of_string", String, Int, int_of_string("int_of_string"))
|> fn(
"float_of_string",
String,
Float,
float_of_string("float_of_string"),
)
|> fn("bool_of_string", String, Bool, bool_of_string("bool_of_string"))
|> fn("abs", Int, Int, abs)
|> fn("abs_float", Float, Float, abs_float)
|> fn("ceil", Float, Float, ceil)
|> fn("floor", Float, Float, floor)
|> fn("exp", Float, Float, exp)
|> fn("log", Float, Float, log)
|> fn("log10", Float, Float, log10)
|> fn("sqrt", Float, Float, sqrt)
|> fn("sin", Float, Float, sin)
|> fn("cos", Float, Float, cos)
|> fn("tan", Float, Float, tan)
|> fn("asin", Float, Float, asin)
|> fn("acos", Float, Float, acos)
|> fn("atan", Float, Float, atan)
|> fn(
"mod",
Prod([Int |> Typ.fresh, Int |> Typ.fresh]),
Int,
int_mod("mod"),
)
|> fn("string_length", String, Int, string_length)
|> fn(
"string_compare",
Prod([String |> Typ.fresh, String |> Typ.fresh]),
Int,
string_compare,
)
|> fn("string_trim", String, String, string_trim)
|> fn(
"string_concat",
Prod([String |> Typ.fresh, List(String |> Typ.fresh) |> Typ.fresh]),
String,
string_concat,
)
|> fn(
"string_sub",
Prod([String |> Typ.fresh, Int |> Typ.fresh, Int |> Typ.fresh]),
String,
string_sub("string_sub"),
)
|> fn(
"string_split",
Prod([String |> Typ.fresh, String |> Typ.fresh]),
List(String |> Typ.fresh),
string_split("string_split"),
);
Fresh.Typ.(
VarMap.empty
|> const("infinity", Float, infinity)
|> const("neg_infinity", Float, neg_infinity)
|> const("nan", Float, nan)
|> const("epsilon_float", Float, epsilon_float)
|> const("pi", Float, pi)
|> const("max_int", Int, max_int)
|> const("min_int", Int, min_int)
|> fn("is_finite", Float, Bool, is_finite)
|> fn("is_infinite", Float, Bool, is_infinite)
|> fn("is_nan", Float, Bool, is_nan)
|> fn("int_of_float", Float, Int, int_of_float)
|> fn("float_of_int", Int, Float, float_of_int)
|> fn("string_of_int", Int, String, string_of_int)
|> fn("string_of_float", Float, String, string_of_float)
|> fn("string_of_bool", Bool, String, string_of_bool)
|> fn("int_of_string", String, Int, int_of_string("int_of_string"))
|> fn(
"float_of_string",
String,
Float,
float_of_string("float_of_string"),
)
|> fn(
"bool_of_string",
String,
Bool,
bool_of_string("bool_of_string"),
)
|> fn("abs", Int, Int, abs)
|> fn("abs_float", Float, Float, abs_float)
|> fn("ceil", Float, Float, ceil)
|> fn("floor", Float, Float, floor)
|> fn("exp", Float, Float, exp)
|> fn("log", Float, Float, log)
|> fn("log10", Float, Float, log10)
|> fn("sqrt", Float, Float, sqrt)
|> fn("sin", Float, Float, sin)
|> fn("cos", Float, Float, cos)
|> fn("tan", Float, Float, tan)
|> fn("asin", Float, Float, asin)
|> fn("acos", Float, Float, acos)
|> fn("atan", Float, Float, atan)
|> fn("mod", Prod([int(), int()]), Int, int_mod("mod"))
|> fn("string_length", String, Int, string_length)
|> fn(
"string_compare",
Prod([string(), string()]),
Int,
string_compare,
)
|> fn("string_trim", String, String, string_trim)
|> fn(
"string_concat",
Prod([string(), list(string())]),
String,
string_concat,
)
|> fn(
"string_sub",
Prod([string(), int(), int()]),
String,
string_sub("string_sub"),
)
|> fn(
"string_split",
Prod([string(), string()]),
List(string()),
string_split("string_split"),
)
);
};

let ctx_init: Ctx.t = {
Expand All @@ -318,13 +316,13 @@ let ctx_init: Ctx.t = {
Ctx.TVarEntry({
name: "$Meta",
id: Id.invalid,
kind: Ctx.Singleton(Sum(meta_cons_map) |> Typ.fresh),
kind: Ctx.Singleton(Fresh.Typ.sum(meta_cons_map)),
});
List.map(
fun
| (name, Const(typ, _)) => Ctx.VarEntry({name, typ, id: Id.invalid})
| (name, Fn(t1, t2, _)) =>
Ctx.VarEntry({name, typ: Arrow(t1, t2) |> Typ.fresh, id: Id.invalid}),
Ctx.VarEntry({name, typ: Fresh.Typ.arrow(t1, t2), id: Id.invalid}),
Pervasives.builtins,
)
|> Ctx.extend(_, meta)
Expand All @@ -345,7 +343,7 @@ let env_init: Environment.t =
fun
| (name, Const(_, d)) => Environment.extend(env, (name, d))
| (name, Fn(_)) =>
Environment.extend(env, (name, BuiltinFun(name) |> fresh)),
Environment.extend(env, (name, Fresh.Exp.builtin_fun(name))),
Environment.empty,
Pervasives.builtins,
);
Loading

0 comments on commit 6df1774

Please sign in to comment.