Typer
Discussions par mois
- ----- 2026 -----
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2025 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2024 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2023 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2022 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2021 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2020 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2019 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2018 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2017 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2016 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
Décembre 2022
- 1 participants
- 1 discussions
[Git][monnier/typer][ja-refl] 3 commits: [WIP] Set the elab context from macros
by Jean-Alexandre Barszcz (@jabarszcz) 22 Déc '22
by Jean-Alexandre Barszcz (@jabarszcz) 22 Déc '22
22 Déc '22
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/511daa3a7b0ff623e81da93527151beb…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/511daa3a7b0ff623e81da93527151beb…
You're receiving this email because of your account on gitlab.com.
1
0