Jean-Alexandre Barszcz pushed to branch master at Stefan / Typer

Commits: bf3c818e by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Add a nix shell

* shell.nix : When using nixpkgs/nixos, run `nix-shell` to get a shell with Typer's dependencies available.

- - - - - c39ff3d5 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Improve the implementation of Sexp.dispatch

* src/elab.ml (sexp_dispatch) : Sexp.dispatch assumed that its arguments were closures. Instead, we use eval_call and also accept constructors, builtins, etc.

- - - - - 7b623a26 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Add the inductive type `Sexp_wrapper` to match on sexps

* btl/pervasive.typer : Add the inductive type `Sexp_wrapper` to wrap the Sexp values in typer code, and the function `Sexp_wrap` to do the wrapping. This makes possible the use of pattern matching to destructure Sexps instead of the more verbose calls to `Sexp_dispatch`.

- - - - - 8419c419 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Fix lexp_whnf when the case scrutinee is a call

* src/opslexp.ml (lexp_whnf) : Make sure that we take the WHNF of the function when the scrutinee of a case expression is a call, before checking that the function is a constructor. Otherwise, expressions like `case (let ... in (constructor ...))` fail to reduce, for example.

- - - - - cc20d841 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Fix some lexp constructor calls where hash-consing has been forgotten

- - - - -

6 changed files:

- btl/pervasive.typer - + shell.nix - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml

Changes:

===================================== btl/pervasive.typer ===================================== @@ -358,6 +358,18 @@ type-impl = lambda (x : List Sexp) ->

type_ = macro type-impl;

+%%%% An inductive type to wrap Sexp + +type Sexp_wrapper + | node Sexp (List Sexp) + | symbol String + | string String + | integer Integer + | float Float + | block Sexp; + +Sexp_wrap s = Sexp_dispatch s node symbol string integer float block; + %%%% Tuples

%% Sample tuple: a module holding Bool and its constructors.

===================================== shell.nix ===================================== @@ -0,0 +1,10 @@ +{ pkgs ? import <nixpkgs> {} }: +pkgs.mkShell { + name = "typer"; + buildInputs = + with pkgs.ocamlPackages; [ + pkgs.gnumake ocaml ocamlbuild findlib utop # tooling + zarith # ocaml libraries + merlin # for emacs + ]; +}

===================================== src/eval.ml ===================================== @@ -552,20 +552,11 @@ and eval_decls (decls: (vname * elexp) list) (String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp) -> Sexp *) and sexp_dispatch loc depth args = - let eval a b = eval a b depth in - let sxp, nd, ctx_nd, - sym, ctx_sym, - str, ctx_str, - it, ctx_it, - flt, ctx_flt, - blk, ctx_blk = match args with - (* FIXME: Don't match against `Closure` to later use `eval`, instead - * pass the value to "funcall". *) - | [sxp; Closure(_, nd, ctx_nd); Closure(_, sym, ctx_sym); - Closure(_, str, ctx_str); Closure(_, it, ctx_it); - Closure(_, flt, ctx_flt); Closure(_, blk, ctx_blk)] -> - sxp, nd, ctx_nd, sym, ctx_sym, str, ctx_str, it, ctx_it, - flt, ctx_flt, blk, ctx_blk + let trace_dum = (Var ((loc, None), -1)) in + let eval_call a b = eval_call loc trace_dum depth a b in + let sxp, nd, sym, str, it, flt, blk = match args with + | [sxp; nd; sym; str; it; flt; blk] -> + sxp, nd, sym, str, it, flt, blk | _ -> error loc "sexp_dispatch expects 7 arguments" in

let sxp = match sxp with @@ -573,34 +564,17 @@ and sexp_dispatch loc depth args = | _ -> value_fatal loc sxp "sexp_dispatch expects a Sexp as 1st arg" in

match sxp with - | Node (op, s) ->( - let rctx = ctx_nd in - let rctx = add_rte_variable vdummy (Vsexp(op)) rctx in - let rctx = add_rte_variable vdummy (o2v_list s) rctx in - match eval nd rctx with - | Closure(_, nd, _) -> eval nd rctx - | _ -> error loc "Node has 2 arguments") - - | Symbol (_ , s) -> - let rctx = ctx_sym in - eval sym (add_rte_variable vdummy (Vstring s) rctx) - | String (_ , s) -> - let rctx = ctx_str in - eval str (add_rte_variable vdummy (Vstring s) rctx) - | Integer (_ , i) -> - let rctx = ctx_it in - eval it (add_rte_variable vdummy (Vinteger (BI.of_int i)) - rctx) - | Float (_ , f) -> - let rctx = ctx_flt in - eval flt (add_rte_variable vdummy (Vfloat f) rctx) + | Node (op, s) -> eval_call nd [Vsexp op; o2v_list s] + | Symbol (_ , s) -> eval_call sym [Vstring s] + | String (_ , s) -> eval_call str [Vstring s] + | Integer (_ , i) -> eval_call it [Vint i] + | Float (_ , f) -> eval_call flt [Vfloat f] | Block (_ , _, _) as b -> (* I think this code breaks what Blocks are. *) (* We delay parsing but parse with default_stt and default_grammar... *) (*let toks = Lexer.lex default_stt s in let s = sexp_parse_all_to_list default_grammar toks (Some ";") in*) - let rctx = ctx_blk in - eval blk (add_rte_variable vdummy (Vsexp b) rctx) + eval_call blk [Vsexp b]

(* -------------------------------------------------------------------------- *) and print_eval_result i lxp =

===================================== src/inverse_subst.ml ===================================== @@ -293,7 +293,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with L.rev ncase) cases in mkInductive (l, label, nargs, ncases) - | Cons (it, name) -> Cons (apply_inv_subst it s, name) + | Cons (it, name) -> mkCons (apply_inv_subst it s, name) | Case (l, e, ret, cases, default) -> mkCase (l, apply_inv_subst e s, apply_inv_subst ret s, SMap.map (fun (l, cargs, e)

===================================== src/lexp.ml ===================================== @@ -402,7 +402,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) L.rev ncase) cases in mkInductive (l, label, nargs, ncases) - | Cons (it, name) -> Cons (mkSusp it s, name) + | Cons (it, name) -> mkCons (mkSusp it s, name) | Case (l, e, ret, cases, default) -> mkCase (l, mkSusp e s, mkSusp ret s, SMap.map (fun (l, cargs, e)

===================================== src/opslexp.ml ===================================== @@ -177,7 +177,10 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = mkCase (l, e, rt, branches, default) in (match e' with | Cons (_, (_, name)) -> reduce name [] - | Call (Cons (_, (_, name)), aargs) -> reduce name aargs + | Call (f, aargs) -> + (match lexp_whnf f ctx with + | Cons (_, (_, name)) -> reduce name aargs + | _ -> mkCase (l, e, rt, branches, default)) | _ -> mkCase (l, e, rt, branches, default)) | Metavar (idx, s, _) -> (match metavar_lookup idx with

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/886a3589162b84e04cf63684239255054...