[Typer] [Git][monnier/typer][ja-refl] 3 commits: [WIP] Set the elab context from macros

Jean-Alexandre Barszcz pushed to branch ja-refl at Stefan / Typer

Commits: a8588787 by Jean-Alexandre Barszcz at 2022-12-22T13:02:13-05:00 [WIP] Set the elab context from macros

- - - - - 6610bc60 by Jean-Alexandre Barszcz at 2022-12-22T13:06:30-05:00 [WIP] Reflect the grammar (precedence table)

- - - - - 3cd133ea by Jean-Alexandre Barszcz at 2022-12-22T13:17:51-05:00 Replace elab's `define-operator` by a macro

- - - - -

5 changed files:

- btl/builtins.typer - btl/pervasive.typer - src/elab.ml - src/env.ml - src/eval.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -408,6 +408,11 @@ gensym = Built-in "gensym" : Unit -> IO Sexp; %% Elab_getenv = Built-in "Elab.getenv" : Unit -> IO Elab_Context;

+%% +%% Set the current context of elaboration +%% +Elab_setenv = Built-in "Elab.setenv" : Elab_Context -> IO Unit; + %% %% Check if a symbol is defined in a particular context %% @@ -445,6 +450,24 @@ Elab_nth-arg' = Built-in "Elab.nth-arg" : String -> Int -> Elab_Context -> Strin %% Elab_arg-pos' = Built-in "Elab.arg-pos" : String -> String -> Elab_Context -> Int;

+%%%% Grammar related stuff + +Option = typecons (Option (ℓ ::: TypeLevel) (a : Type_ ℓ)) (none) (some a); +some = datacons Option some; +none = datacons Option none; + +Operator = typecons Operator (mkOperator String (l : Option Integer) (r : Option Integer)); +mkOperator = datacons Operator mkOperator; + +PrecTable = typecons PrecTable (mkPrecTable (List Operator)); +mkPrecTable = datacons PrecTable mkPrecTable; + +Elab_get-grammar : Elab_Context -> PrecTable; +Elab_get-grammar = Built-in "Elab.get-grammar"; + +Elab_set-grammar : Elab_Context -> PrecTable -> Elab_Context; +Elab_set-grammar = Built-in "Elab.set-grammar"; + %%%% Unit test helper IO

%%

===================================== btl/pervasive.typer ===================================== @@ -32,10 +32,6 @@

%%%% `Option` type

-Option = typecons (Option (ℓ ::: TypeLevel) (a : Type_ ℓ)) (none) (some a); -some = datacons Option some; -none = datacons Option none; - optionally : (?a -> ?b) -> ?b -> Option ?a -> ?b; optionally func = lambda def -> @@ -481,6 +477,48 @@ type LList (a : Type) (n : Int) | vnil (p ::: Eq n (Integer->Int 0)) | vcons a (LList a ?n1) (p ::: Eq n (Int_+ ?n1 (Integer->Int 1)));

+%%%% define-operator + +define-operator-impl : List Sexp -> IO Sexp; +define-operator-impl args = + let add_op' : String -> Option Integer -> Option Integer -> IO Sexp; + add_op' op l r = + IO_bind (Elab_getenv ()) + (lambda ctx -> + case Elab_get-grammar ctx + | mkPrecTable ls => + let grm = mkPrecTable (cons (mkOperator op l r) ls) in + IO_bind (Elab_setenv (Elab_set-grammar ctx grm)) + (lambda _ -> IO_return (quote ()))); + add_op : Sexp -> Sexp -> Sexp -> IO Sexp; + add_op op l r = + case Sexp_wrap op + | string op => + (case Sexp_wrap l + | integer l => + (case Sexp_wrap r + | integer r => add_op' op (some l) (some r) + | symbol _ => add_op' op (some l) none + | _ => IO_return Sexp_error) + | symbol _ => + (case Sexp_wrap r + | integer r => add_op' op none (some r) + | symbol _ => add_op' op none none + | _ => IO_return Sexp_error) + | _ => IO_return Sexp_error) + | _ => IO_return Sexp_error; + in case args + | cons op args' => + (case args' + | cons l args'' => + (case args'' + | cons r nil => add_op op l r + | _ => IO_return Sexp_error) + | _ => IO_return Sexp_error) + | _ => IO_return Sexp_error; + +define-operator = macro define-operator-impl; + %%%% If

define-operator "if" () 2;

===================================== src/elab.ml ===================================== @@ -331,20 +331,6 @@ let mkDummy_infer ctx loc = let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in (mkDummy_check ctx loc t, t)

-let sdform_define_operator (ctx : elab_context) loc sargs : elab_context = - match sargs with - | [String (_, name); l; r] - -> let level s = match s with - | Symbol (_, "") -> None - | Integer (_, n) -> Some (Z.to_int n) - | _ -> sexp_error (sexp_location s) "Expecting an integer or ()"; None in - let grm = ectx_get_grammar ctx in - ectx_set_grammar (SMap.add name (level l, level r) grm) ctx - | [o; _; _] - -> sexp_error (sexp_location o) "Expecting a string"; ctx - | _ - -> sexp_error (sexp_location loc) "define-operator expects 3 argument"; ctx - let sform_dummy_ret ctx loc = let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in (newMetavar (ectx_to_lctx ctx) dummy_scope_level @@ -1022,7 +1008,7 @@ and elab_macro_call arg |> sexp_string |> trace_macro ~location:(sexp_location location) {|input %d: %s|} i) args);

- let sxp = lexp_expand_macro location func args ctx (Some t) in + let sxp, _ = lexp_expand_macro false location func args ctx (Some t) in if !macro_tracing_enabled then trace_macro ~location:(sexp_location location) {|output: %s|} (sexp_string sxp);

@@ -1178,8 +1164,8 @@ and lexp_eval ectx e = "Exception happened during evaluation:"; raise exc

-and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) - : sexp = +and lexp_expand_macro mutable_ctxt loc macro_funct sargs ctx (_ot : ltype option) + : sexp * (elab_context option) =

(* Build the function to be called *) let macro_expand = PR.get_predef' "Macro_expand" ctx in @@ -1190,6 +1176,8 @@ and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) let macro = lexp_eval ctx macro_funct in let args = [macro; sexp_list_to_val sargs] in

+ EV.set_getenv ctx; + EV.set_mutable_env mutable_ctxt; (* FIXME: Make a proper `Var`. *) let value = EV.eval_call (sexp_location loc) (EL.Var ((dsinfo, Some "expand_macro"), 0)) ([], []) macro_expand args in @@ -1197,11 +1185,11 @@ and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) | Vcommand cmd -> let v = cmd () in (match val_to_sexp v with - | Some sxp -> sxp + | Some sxp -> sxp, if mutable_ctxt then Some (EV.get_getenv ()) else None | _ -> value_fatal (sexp_location loc) v "Macro `%s` should return an IO sexp" - (lexp_string macro_funct)) + (lexp_string macro_funct), None) | v -> value_fatal (sexp_location loc) v "Macro `%s` should return an IO" - (lexp_string macro_funct) + (lexp_string macro_funct), None

(* Print each generated decls *) @@ -1424,17 +1412,19 @@ and lexp_decls_1 else if (OL.conv_p lctx t (PR.get_predef' "Macro" nctx)) then (* expand macro and get the generated declarations *) let lxp, _ltp = infer sxp nctx in - let sdecl' = lexp_expand_macro sxp lxp sargs nctx None in - recur [sdecl'] nctx pending_decls pending_defs + (match lexp_expand_macro true sxp lxp sargs nctx None with + | sdecl', Some nctx' -> + recur [sdecl'] nctx' pending_decls pending_defs + | sdecl', None -> + recur [sdecl'] nctx pending_decls pending_defs) else ( error ~loc:(sexp_location sxp) "Invalid declaration syntax"; recur [] nctx pending_decls pending_defs )

- in (EV.set_getenv nctx; - let res = lexp_decls_1 sdecls tokens nctx - pending_decls pending_defs in - (Log.stop_on_error (); res)) + in let res = lexp_decls_1 sdecls tokens nctx + pending_decls pending_defs in + (Log.stop_on_error (); res)

(* Why is the return value a list of list? - each `(vname * lexp * ltype)` is a definition @@ -1992,7 +1982,6 @@ let register_special_forms () = ]; List.iter add_special_decl_form [ - ("define-operator", sdform_define_operator); ("typeclass", sdform_typeclass); ("instance", sdform_instance true); ("not-instance", sdform_instance false);

===================================== src/env.ml ===================================== @@ -35,6 +35,7 @@ open Printf open Fmt (* make_title, table util *)

open Sexp +open Grammar

open Elexp module M = Myers @@ -54,6 +55,7 @@ let str_idx idx = "[" ^ (string_of_int idx) ^ "]" type 'a type_repr = | Rsexp : sexp type_repr | Rlist : (value_type list) type_repr + | Rprecs : grammar type_repr

(* Gadts + record parameter for existential quantification & mutual recursion *) and conslike = @@ -95,6 +97,7 @@ let cast_conslike_val : type t. t type_repr -> conslike -> t option = match typ, c.typ with | Rsexp, Rsexp -> Some c.v | Rlist, Rlist -> Some c.v + | Rprecs, Rprecs -> Some c.v | _ -> None

let conslike_eq (Conslike c1) c2 : bool = @@ -354,3 +357,57 @@ let rec val_to_sexp (v : value_type) : sexp option = | _ -> None with Invalid_argument _ -> None) | _ -> None + +let val_to_option (v : value_type) : (value_type option) option = + match v with + | Vcons ((_, "some"), [x]) -> Some (Some x) + | Vcons ((_, "none"), []) -> Some None + | _ -> None + +let option_to_val (ov : value_type option) : value_type = + match ov with + | Some v -> Vcons ((dloc, "some"), [v]) + | None -> Vcons ((dloc, "none"), []) + +let grammar_to_val (g : grammar) : value_type = + let operator_to_val (n, (l, r)) = + Vcons ((dloc, "mkOperator"), + [Vstring n; + option_to_val (Option.map (fun x -> Vinteger (Z.of_int x)) l); + option_to_val (Option.map (fun x -> Vinteger (Z.of_int x)) r)]) in + let unwrap_grm (g : grammar) : (symbol * value_type list) = + (dloc, "mkPrecTable"), + [list_to_val (List.map operator_to_val (SMap.bindings g))] in + Vconslike (Conslike { + v = g; + typ = Rprecs; + unwrap = unwrap_grm; + eq = SMap.equal (==); + to_string = fun g -> + let (sym, args) = unwrap_grm g in + value_string (Vcons (sym, args)); + }) + +let val_to_grammar (v : value_type) : grammar option = + let val_to_int (v : value_type) : int option = + match v with + | Vinteger i -> Some (Z.to_int i) + | _ -> None in + let val_to_operator (v : value_type) : + (string * (int option * int option)) option = + match v with + | Vcons ((_, "mkOperator"), [Vstring n; l; r]) -> + (match val_to_option l, val_to_option r with + | Some l, Some r -> Some (n, (Option.bind l val_to_int, + Option.bind r val_to_int)) + | _ -> None) + | _ -> None in + match v with + | Vconslike c -> cast_conslike_val Rprecs c + | Vcons ((_, "mkPrecTable"), [l]) -> + (match val_to_list l with + | Some l -> Some ((List.map (fun op -> Option.get (val_to_operator op)) l) + |> List.to_seq |> SMap.of_seq) + | None -> None) + | _ -> None +

===================================== src/eval.ml ===================================== @@ -139,8 +139,12 @@ let tunit = Vcons ((dloc, "unit"), []) and then undefine it. The thing is elab_context may not exist at runtime so I must save it somewhere if the Elab.* function persist. *) let macro_monad_elab_context = ref empty_elab_context +let macro_monad_mutable_context = ref false

let set_getenv (ectx : elab_context) = macro_monad_elab_context := ectx +let get_getenv () : elab_context = !macro_monad_elab_context + +let set_mutable_env (b : bool) = macro_monad_mutable_context := b

(* * Builtins @@ -809,9 +813,31 @@ let gensym = let count = ref 0 in | _ -> error loc "gensym takes a Unit as argument")

let getenv loc _depth args_val = match args_val with - | [_v] -> Vcommand (fun () -> Velabctx !macro_monad_elab_context) + | [_v] -> Vcommand (fun () -> Velabctx (get_getenv ())) | _ -> error loc "getenv takes a single Unit as argument"

+let setenv loc _depth args_val = + match !macro_monad_mutable_context, args_val with + | true, [Velabctx ectx] -> + Vcommand (fun () -> set_getenv ectx; Vcons ((dloc, "unit"), [])) + | false, _ -> error loc "Cannot setenv unless macro call is a declaration" + | _ -> error loc "setenv takes an Elab_Context as argument" + +let get_grammar loc _depth args_val = match args_val with + | [Velabctx ectx] -> + grammar_to_val (ectx_get_grammar ectx) + | _ -> error loc "Elab.get_grammar takes an Elab_Context as argument" + +let set_grammar loc _depth args_val = + let error_message = + "Elab.set_grammar takes an Elab_Context and a PrecTable as arguments" in + match args_val with + | [Velabctx ectx; v] -> + (match val_to_grammar v with + | Some g -> Velabctx (ectx_set_grammar g ectx) + | None -> error loc "%s" error_message) + | _ -> error loc "%s" error_message + let is_bound loc _depth args_val = match args_val with | [Vstring name; Velabctx ectx] -> o2v_bool (try (ignore (senv_lookup name ectx); true) @@ -1078,6 +1104,9 @@ let register_builtin_functions () = ("Ref.write" , ref_write, 2); ("gensym" , gensym, 1); ("Elab.getenv" , getenv, 1); + ("Elab.setenv" , setenv, 1); + ("Elab.get-grammar", get_grammar, 1); + ("Elab.set-grammar", set_grammar, 2); ("Elab.isbound" , is_bound, 2); ("Elab.isconstructor", is_constructor, 2); ("Elab.is-nth-erasable", is_nth_erasable, 3);

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/511daa3a7b0ff623e81da93527151beb0...