Février 2022 - Typer - mailman.iro.umontreal.ca

Tracer l'expansion de macros
by Simon Génier 08 Mar '22

08 Mar '22

Salut, Je déboguais un petit problème de macro et j'ai fait un truc pour imprimer quel macro est étendu (??), quels sont ses arguments et quel est le résultat. Je me suis dit que ça pourrait être utile pour plus tard alors je l'ai mis dans une patch. https://gitlab.com/monnier/typer/-/commit/29c8adedee2eef35b4fcc775d871bb9f5… Vous pouvez le tester avec dune exec ./typer.exe -- -v -v -Vmacro-expansion ./samples/nat.typer Simon

2 1

Numéros de ligne
by Simon Génier 08 Mar '22

08 Mar '22

Salut, J'avais remarqué que les numéros de ligne étaient incorrects, toujours off de 1. Je viens de prendre le temps de regarder ça et j'ai une patch que j'aimerais merger si vous voulez la réviser. https://gitlab.com/monnier/typer/-/commit/e0d8110c35cd9cdfd69f87233d03c25ac… Le changement lui-même est un simple - 1 dans source.ml. Je me suis laissé un peu emporter par les tests, où j'ai ajouté un module pour avoir des bons messages d'erreur quand on compare des listes. Dites-moi si vous aimez, si oui je peux changer pas mal d'autres tests de sexps, lexps, etc pour utiliser ce module et effacer pas mal de code. Justement, sur ce sujet, un truc super laborieux en Ocaml est de réécrire pour chaque type une fonction pour les afficher. Je sais qu'on veux éviter les dépendances, mais je viens de me rendre compte de quelque chose. https://ppxlib.readthedocs.io/en/latest/ppx-for-end-users.html#dropping-ppx… Ppxlib supporte la génération de code sans dépendances à ppxlib. C'est-à-dire que le code généré va continuer à fonctionner même si on l'enlève, par exemple s'il ne marche plus avec une version future de Ocaml. Qu'est-ce que vous en pensez? Finalement, un truc qui me dérange est le traitement différent de -> et =, plus particulièrement la différence avec les retours de chariot. On brise le ligne avant le ->, mais après le =. match a with | B -> c; d let a = b La raison est que -> est un opérateur, mais n'est-ce pas plus un séparateur comme le = ? match a with | B -> c; d On sauve quand même deux colonnes d'espace horizontal, ce qui n'est pas négligeable quand on veut respecter les 80 colonnes. Surtout que deux matchs imbriqués n'est pas rare. Dites-moi ce que vous en pensez. Simon

2 1

[Git][monnier/typer][instance-args] 9 commits: * src/elab.ml: Handle sdforms in a common way.
by Jean-Alexandre Barszcz (＠jabarszcz) 24 Fév '22

24 Fév '22

Jean-Alexandre Barszcz pushed to branch instance-args at Stefan / Typer Commits: 5bb8561d by Jean-Alexandre Barszcz at 2022-02-24T18:07:29-05:00 * src/elab.ml: Handle sdforms in a common way. - - - - - 7a9f2d6b by Jean-Alexandre Barszcz at 2022-02-24T18:07:29-05:00 * src/debruijn.ml: Add a type class context to the elab context. * src/elab.ml: Add the `typeclass` sdform that adds a type to the set of typeclasses in the typeclass context. Add the `instance` and `not-instance` sdforms that set the instance flag for given variables in the typeclass context. Add the `bind-instances` and `dont-bind-instances` sdforms that set the default instance flag for new variables. * src/instargs.ml: New source file for things related to instance arguments. - - - - - 3aea7f2b by Jean-Alexandre Barszcz at 2022-02-24T18:07:29-05:00 * tests/instargs_test.ml: New file, test the type class context. - - - - - 2c66ad00 by Jean-Alexandre Barszcz at 2022-02-24T18:07:29-05:00 * src/elab.ml: Save metavars' elaboration contexts for resolution. * src/instargs.ml: Keep a table of resolution contexts for instance metavariables. - - - - - 97b66381 by Jean-Alexandre Barszcz at 2022-02-24T18:07:29-05:00 * src/instargs: Implement instance resolution. * src/elab.ml: Resolve instances before every generalization. (lexp_check_decls): Resolve instances for recursive definitions. (lexp_expr_str): Resolve instances when elaborating from a string. * src/REPL.ml: Resolve and generalize expressions in the REPL. - - - - - b53381b0 by Jean-Alexandre Barszcz at 2022-02-24T18:07:29-05:00 * src/unification.ml (unify_call) : Return CKImpossible when we can. - - - - - bb13299a by Jean-Alexandre Barszcz at 2022-02-24T18:07:29-05:00 Make integer literals polymorphic using type classes * btl/poly-lits.typer: New file implementing polymorphic integer literals through the "typer-immediate" hook and type classes. * btl/pervasive.typer: Use the new definition of "typer-immediate". - - - - - c946942e by Jean-Alexandre Barszcz at 2022-02-24T18:07:29-05:00 Change integer literals to have type Integer by default - - - - - de75a4da by Jean-Alexandre Barszcz at 2022-02-24T18:07:29-05:00 Make `do` polymorphic with a `Monad` class. - - - - - 21 changed files: - btl/case.typer - btl/do.typer - + btl/monads.typer - btl/pervasive.typer - + btl/poly-lits.typer - + samples/nats.typer - src/REPL.ml - src/debruijn.ml - src/elab.ml - src/eval.ml - + src/instargs.ml - src/myers.ml - src/opslexp.ml - src/unification.ml - tests/dune - tests/elab_test.ml - tests/eval_test.ml - + tests/instargs_test.ml - tests/macro_test.ml - tests/unify_test.ml - tests/utest_lib.ml Changes: ===================================== btl/case.typer ===================================== @@ -407,7 +407,7 @@ introduced-vars pat = let %% %% error used in Sexp_dispatch %% - serr = lambda _ -> IO_return (pair 0 nil); + serr = lambda _ -> IO_return (pair (0 : Int) nil); %% %% List of kind of pattern argument ===================================== btl/do.typer ===================================== @@ -2,16 +2,19 @@ %% Here's an example : %% -%% fun = do { -%% str <- return "\n\tHello world!\n\n"; +%% fun = do IO { +%% str <- pure "\n\tHello world!\n\n"; %% print str; %% }; %% -%% `str` is bind by macro, +%% `str` is bound by macro, %% %% `fun` is a command, %% %% `do` may contain `do` because it returns a command. +%% +%% `IO` is given as an optional first argument to specify the monad +%% used (since inference is often not able to find it). %% %% Operator of assignment in `do` block @@ -91,8 +94,8 @@ in node; %% %% The idea of the macro is : %% -%% IO_bind a-op (lambda a-sym -> [next command or return a-sym]) -%% IO_bind a-op (lambda a-sym -> (IO_bind b-op (lambda b-sym -> [next command or return b-sym]))) +%% bind a-op (lambda a-sym -> [next command or return a-sym]) +%% bind a-op (lambda a-sym -> (bind b-op (lambda b-sym -> [next command or return b-sym]))) %% %% this way a-sym is defined within b-op and so on %% a-sym is now just `a` and not `IO a` @@ -105,8 +108,16 @@ in node; %% Takes the list of command inside `do` block %% This is the `main` of macro `do` %% -set-fun : List Sexp -> Sexp; -set-fun args = let +set-fun : String -> String -> Option Sexp -> List Sexp -> Sexp; +set-fun bind_name return_name omonad args = let + + explicit_arg name sexp = + (Sexp_node (Sexp_symbol "_:=_") (cons (Sexp_symbol name) (cons sexp nil))); + + add_explicit_arg name opt list = + optionally (lambda arg -> cons (explicit_arg name arg) list) list opt; + + add_omonad_arg = add_explicit_arg "M" omonad; helper : Sexp -> List Sexp -> Sexp; helper lsym args = case args @@ -116,11 +127,14 @@ set-fun args = let op = get-op s; - in Sexp_node (Sexp_symbol "IO_bind") (cons (op) - (cons (Sexp_node (Sexp_symbol "lambda_->_") (cons sym (cons (helper sym ss) nil))) nil)) + in Sexp_node + (Sexp_symbol bind_name) + (add_omonad_arg + (cons (op) (cons (Sexp_node (Sexp_symbol "lambda_->_") + (cons sym (cons (helper sym ss) nil))) nil))) ) - | nil => Sexp_node (Sexp_symbol "IO_return") (cons lsym nil); + | nil => Sexp_node (Sexp_symbol return_name) (add_omonad_arg (cons lsym nil)); in helper (Sexp_symbol "") args; % return Unit if no command given @@ -129,9 +143,19 @@ in helper (Sexp_symbol "") args; % return Unit if no command given %% Serie of command %% -do = macro (lambda args -> - IO_bind (Elab_getenv unit) - (lambda ctx -> IO_return (set-fun (get-decl ctx args)))); +do-impl bind_name return_name args = + let p = case args + | cons x xs => (case xs + | cons _ _ => + pair (some x) xs + | _ => pair none args) + | _ => pair none args; + omonad = p.fst; + args = p.snd; + in IO_bind (Elab_getenv unit) + (lambda ctx -> IO_return (set-fun bind_name return_name omonad (get-decl ctx args))); + +do = macro (do-impl "IO_bind" "IO_return"); %% %% Next are example command ===================================== btl/monads.typer ===================================== @@ -0,0 +1,22 @@ +type Monad (M : Type -> Type) : Type_ (s z) + | mkMonad (bind : (a : Type) ≡> (b : Type) ≡> + M a -> (a -> M b) -> M b) + (pure : (a : Type) ≡> a -> M a); +typeclass Monad; +bind = case ?monad | mkMonad bind pure => bind; +pure = case ?monad | mkMonad bind pure => pure; + +IO_monad : Monad IO; +IO_monad = mkMonad (M := IO) (bind := IO_bind) (pure := IO_return); + +Option_bind : (a : Type) ≡> (b : Type) ≡> Option a -> (a -> Option b) -> Option b; +Option_bind oa aob = + case oa + | some a => aob a + | none => none; + +Option_pure : (a : Type) ≡> a -> Option a; +Option_pure = some (ℓ := ##TypeLevel_z); + +Option_monad : Monad Option; +Option_monad = mkMonad (M := Option (ℓ := ##TypeLevel_z)) (bind := Option_bind) (pure := Option_pure) ===================================== btl/pervasive.typer ===================================== @@ -36,13 +36,21 @@ 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 -> + lambda opt -> + case opt + | some a => func a + | none => def; + %%%% List functions List_length : List ?a -> Int; % Recursive defs aren't generalized :-( List_length xs = case xs - | nil => 0 + | nil => (Integer->Int 0) | cons hd tl => - (1 + (List_length tl)); + (Int_+ (Integer->Int 1) (List_length tl)); %% ML's typical `head` function is not total, so can't be defined %% as-is in Typer. There are several workarounds: @@ -80,9 +88,9 @@ List_nth : Int -> List ?a -> ?a -> ?a; List_nth = lambda n -> lambda xs -> lambda d -> case xs | nil => d | cons x xs - => case Int_<= n 0 + => case Int_<= n (Integer->Int 0) | true => x - | false => List_nth (n - 1) xs d; + | false => List_nth (Int_- n (Integer->Int 1)) xs d; %%%% A more flexible `lambda` @@ -155,8 +163,8 @@ List_mapi f xs = let helper : (a -> Int -> b) -> Int -> List a -> List b; helper f i xs = case xs | nil => nil - | cons x xs => cons (f x i) (helper f (i + 1) xs); -in helper f 0 xs; + | cons x xs => cons (f x i) (helper f (Int_+ i (Integer->Int 1)) xs); +in helper f (Integer->Int 0) xs; List_map2 : (?a -> ?b -> ?c) -> List ?a -> List ?b -> List ?c; List_map2 f xs ys = case xs @@ -175,7 +183,7 @@ List_fold2 f o xs ys = case xs %% Is argument List empty? List_empty : List ?a -> Bool; -List_empty xs = Int_eq (List_length xs) 0; +List_empty xs = Int_eq (List_length xs) (Integer->Int 0); %%% Good 'ol combinators @@ -320,7 +328,7 @@ type-impl = lambda (x : List Sexp) -> let single-colon-arg = (Sexp_node (Sexp_symbol "_:_") (cons (List_head Sexp_error ss) - (cons (List_nth 1 ss Sexp_error) nil))); + (cons (List_nth (Integer->Int 1) ss Sexp_error) nil))); arrow-args = (cons single-colon-arg (cons arrow-type nil)) in case (Sexp_eq s (Sexp_symbol "_:_")) | true => Sexp_node (Sexp_symbol "_->_") arrow-args @@ -356,8 +364,8 @@ type-impl = lambda (x : List Sexp) -> | true => get-list head+ | false => cons head+ (cons (Sexp_symbol "Type") nil); - head = List_nth 0 head-pair Sexp_error; - type-type = List_nth 1 head-pair Sexp_error; + head = List_nth (Integer->Int 0) head-pair Sexp_error; + type-type = List_nth (Integer->Int 1) head-pair Sexp_error; type-name = get-name head; type-args = get-list head; @@ -470,8 +478,8 @@ Decidable = typecons (Decidable (prop : Type_ ?ℓ)) %% Testing generalization in inductive type constructors. LList : Type -> Int -> Type; %FIXME: `LList : ?` should be sufficient! type LList (a : Type) (n : Int) - | vnil (p ::: Eq n 0) - | vcons a (LList a ?n1) (p ::: Eq n (?n1 + 1)); %FIXME: Unsound wraparound! + | vnil (p ::: Eq n (Integer->Int 0)) + | vcons a (LList a ?n1) (p ::: Eq n (Int_+ ?n1 (Integer->Int 1))); %%%% If @@ -481,9 +489,9 @@ define-operator "else" 1 66; if_then_else_ = macro (lambda args -> - let e1 = List_nth 0 args Sexp_error; - e2 = List_nth 1 args Sexp_error; - e3 = List_nth 2 args Sexp_error; + let e1 = List_nth (Integer->Int 0) args Sexp_error; + e2 = List_nth (Integer->Int 1) args Sexp_error; + e3 = List_nth (Integer->Int 2) args Sexp_error; in IO_return (quote (case uquote e1 | true => uquote e2 | false => uquote e3))); @@ -549,7 +557,7 @@ in case (String_eq r "_") %% Elab_arg-pos a b c = let r = Elab_arg-pos' a b c; -in case (Int_eq r (-1)) +in case (Int_eq r (Integer->Int -1)) | true => (none) | false => (some r); @@ -557,6 +565,34 @@ in case (Int_eq r (-1)) %%%% Common library %%%% +%% +%% Polymorphic literals +%% + +%% FIXME: It would be useful to have a way to "open" modules. +poly-lits = load "btl/poly-lits.typer"; +typer-immediate = poly-lits.typer-immediate; +FromInteger = poly-lits.FromInteger; +mkFromInteger = poly-lits.mkFromInteger; +fromInteger = poly-lits.fromInteger; +IntFromInteger = poly-lits.IntFromInteger; +IntegerFromInteger = poly-lits.IntegerFromInteger; +instance IntFromInteger IntegerFromInteger; +typeclass FromInteger; + +%% +%% Monads +%% + +monads = load "btl/monads.typer"; +Monad = monads.Monad; +bind = monads.bind; +pure = monads.pure; +IO_monad = monads.IO_monad; +Option_monad = monads.Option_monad; +instance IO_monad Option_monad; +typeclass Monad; + %% %% `<-` operator used in macro `do` and for tuple assignment %% @@ -574,7 +610,9 @@ list = load "btl/list.typer"; %% e.g.: %% do { IO_return true; }; %% -do = let lib = load "btl/do.typer" in lib.do; +do-lib = load "btl/do.typer"; +do-impl = do-lib.do-impl; +do = do-lib.do; %% %% Module containing various macros for tuple @@ -683,4 +721,8 @@ in IO_return (Sexp_dispatch (List_nth 0 args Sexp_error) (lambda _ -> ret)) ); +%%%% Generalized do + +do = macro (do-impl "bind" "pure"); + %%% pervasive.typer ends here. ===================================== btl/poly-lits.typer ===================================== @@ -0,0 +1,24 @@ +type (FromInteger (α : Type)) + | mkFromInteger (fromInteger : Integer -> α); + +typeclass FromInteger; + +fromInteger = lambda inst => case inst | mkFromInteger fromInteger => fromInteger; + +typer-immediate = + macro (lambda args -> + let deflt = + IO_return (Sexp_node (Sexp_symbol "##typer-immediate") args); + in case args + | cons sexp nil => + (case Sexp_wrap sexp + | integer i => + IO_return (quote (fromInteger (##typer-immediate (uquote sexp)))) + | _ => deflt) + | _ => deflt); + +IntegerFromInteger : FromInteger Integer; +IntegerFromInteger = mkFromInteger I; + +IntFromInteger : FromInteger Int; +IntFromInteger = mkFromInteger Integer->Int; ===================================== samples/nats.typer ===================================== @@ -0,0 +1,12 @@ +type Nat + | Z + | S Nat; + +Integer->Nat : Integer -> Nat; +Integer->Nat i = + if Integer_< 0 i then + S (Integer->Nat (Integer_- i 1)) + else Z; + +NatFromInteger : FromInteger Nat; +NatFromInteger = mkFromInteger Integer->Nat; ===================================== src/REPL.ml ===================================== @@ -136,6 +136,11 @@ let eval_interactive let ldecls, ectx' = Elab.lexp_p_decls decls [] ectx in let lexprs = Elab.lexp_parse_all exprs ectx' in + + let generalize_lexp ctx lxp = + Elab.resolve_instances_and_generalize ctx lxp Elab.wrapLambda lxp in + let lexprs = List.map (generalize_lexp ectx') lexprs in + List.iter (fun lexpr -> ignore (OL.check (ectx_to_lctx ectx') lexpr)) lexprs; List.iter interactive#process_decls ldecls; ===================================== src/debruijn.ml ===================================== @@ -145,26 +145,31 @@ type meta_scope * lctx_length (* Length of ctx when the scope is added. *) * (meta_id SMap.t ref) (* Metavars already known in this scope. *) +type typeclass_ctx + = (ltype * lctx_length) list (* the list of type classes *) + * bool (* true if new bindings can be instances *) + * bool M.myers (* Are bindings instances ? Same shape as lctx *) + (* This is the *elaboration context* (i.e. a context that holds * a lexp context plus some side info. *) type elab_context - = Grammar.grammar * senv_type * lexp_context * meta_scope + = Grammar.grammar * senv_type * lexp_context * meta_scope * typeclass_ctx let get_size (ctx : elab_context) - = let (_, (n, _), lctx, _) = ctx in + = let (_, (n, _), lctx, _, _) = ctx in assert (n = M.length lctx); n let ectx_to_grm (ectx : elab_context) : Grammar.grammar = - let (grm,_, _, _) = ectx in grm + let (grm,_, _, _, _) = ectx in grm (* Extract the lexp context from the context used during elaboration. *) let ectx_to_lctx (ectx : elab_context) : lexp_context = - let (_,_, lctx, _) = ectx in lctx + let (_,_, lctx, _, _) = ectx in lctx -let ectx_to_scope_level ((_, _, _, (sl, _, _)) : elab_context) : scope_level +let ectx_to_scope_level ((_, _, _, (sl, _, _), _) : elab_context) : scope_level = sl -let ectx_local_scope_size ((_, (_n, _), _, (_, slen, _)) as ectx) : int +let ectx_local_scope_size ((_, (_n, _), _, (_, slen, _), _) as ectx) : int = get_size ectx - slen (* Public methods: DO USE @@ -172,10 +177,11 @@ let ectx_local_scope_size ((_, (_n, _), _, (_, slen, _)) as ectx) : int let empty_senv = (0, SMap.empty) let empty_lctx = M.nil +let empty_tcctx = ([], false, M.nil) let empty_elab_context : elab_context = (Grammar.default_grammar, empty_senv, empty_lctx, - (0, 0, ref SMap.empty)) + (0, 0, ref SMap.empty), empty_tcctx) (* senv_lookup caller were using Not_found exception *) exception Senv_Lookup_Fail of (string list) @@ -183,7 +189,7 @@ let senv_lookup_fail relateds = raise (Senv_Lookup_Fail relateds) (* Return its current DeBruijn index. *) let senv_lookup (name: string) (ctx: elab_context): int = - let (_, (n, map), _, _) = ctx in + let (_, (n, map), _, _, _) = ctx in try n - (SMap.find name map) - 1 with Not_found -> let get_related_names (_n : db_ridx) name map = @@ -220,13 +226,22 @@ let lexp_ctx_cons (ctx : lexp_context) d v t = let lctx_extend (ctx : lexp_context) (def: vname) (v: varbind) (t: lexp) = lexp_ctx_cons ctx def v t +let tcctx_extend ((tcs, inst_def, insts) : typeclass_ctx) = + tcs, inst_def, (M.cons inst_def insts) + +let tcctx_extend_rec (n : int) ((tcs, inst_def, insts) : typeclass_ctx) = + let rec cons_n n x l = + if n = 0 then l else + M.cons x (cons_n (n - 1) x l) in + tcs, inst_def, (cons_n n inst_def insts) + let env_extend_rec (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = let (_loc, oname) = def in - let (grm, (n, map), env, sl) = ctx in + let (grm, (n, map), env, sl, tcctx) = ctx in let nmap = match oname with None -> map | Some name -> SMap.add name n map in (grm, (n + 1, nmap), lexp_ctx_cons env def v t, - sl) + sl, tcctx_extend tcctx) let ectx_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec ctx def v t @@ -240,28 +255,48 @@ let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) = ctx let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) = - let (grm, (n, senv), lctx, sl) = ctx in + let (grm, (n, senv), lctx, sl, tcctx) = ctx in + let len = List.length defs in let senv', _ = List.fold_left (fun (senv, i) ((_, oname), _, _) -> (match oname with None -> senv | Some name -> SMap.add name i senv), i + 1) (senv, n) defs in - (grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl) + (grm, (n + len, senv'), lctx_extend_rec lctx defs, sl, + tcctx_extend_rec len tcctx) let ectx_new_scope (ectx : elab_context) : elab_context = - let (grm, senv, lctx, (scope, _, rmmap)) = ectx in - (grm, senv, lctx, (scope + 1, Myers.length lctx, ref (!rmmap))) + let (grm, senv, lctx, (scope, _, rmmap), tcctx) = ectx in + (grm, senv, lctx, (scope + 1, Myers.length lctx, ref (!rmmap)), tcctx) let ectx_get_scope (ectx : elab_context) : meta_scope = - let (_, _, _, sl) = ectx in sl + let (_, _, _, sl, _) = ectx in sl let ectx_get_grammar (ectx : elab_context) : Grammar.grammar = - let (grm, _, _, _) = ectx in grm + let (grm, _, _, _, _) = ectx in grm let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index ctx +let ectx_to_tcctx (ectx : elab_context) : typeclass_ctx = + let (_, _, _, _, tcctx) = ectx in tcctx + +let ectx_add_typeclass (ectx : elab_context) (t : ltype) : elab_context = + let (grm, senv, lctx, sl, (tcs, inst_def, insts)) = ectx in + let ntcctx = ((t, get_size ectx) :: tcs, inst_def, insts) in + (grm, senv, lctx, sl, ntcctx) + +let ectx_set_inst (ectx : elab_context) (index : int) (inst : bool) + : elab_context = + let (grm, senv, lctx, sl, (tcs, inst_def, insts)) = ectx in + let ntcctx = (tcs, inst_def, M.set_nth index inst insts) in + (grm, senv, lctx, sl, ntcctx) + +let ectx_set_inst_def (ectx : elab_context) (inst_def : bool) : elab_context = + let (grm, senv, lctx, sl, (tcs, _, insts)) = ectx in + (grm, senv, lctx, sl, (tcs, inst_def, insts)) + let print_lexp_ctx_n (ctx : lexp_context) (ranges : (int * int) list) = print_string (make_title " LEXP CONTEXT "); ===================================== src/elab.ml ===================================== @@ -56,6 +56,7 @@ open Grammar module BI = Builtin module Unif = Unification +module Inst = Instargs module OL = Opslexp module EL = Elexp @@ -107,16 +108,27 @@ type special_forms_map = (elab_context -> location -> sexp list -> ltype option -> (lexp * sform_type)) SMap.t +type special_decl_forms_map = + (elab_context -> location -> sexp list -> elab_context) SMap.t + let special_forms : special_forms_map ref = ref SMap.empty +let special_decl_forms : special_decl_forms_map ref = ref SMap.empty let type_special_form = BI.new_builtin_type "Special-Form" type0 let add_special_form (name, func) = BI.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form)); special_forms := SMap.add name func (!special_forms) +let add_special_decl_form (name, func) = + BI.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form)); + special_decl_forms := SMap.add name func (!special_decl_forms) + let get_special_form name = SMap.find name (!special_forms) +let get_special_decl_form name = + SMap.find name (!special_decl_forms) + (* Used for sform_load because sform are * added before default context's function. *) let sform_default_ectx = ref empty_elab_context @@ -263,6 +275,36 @@ let newMetavar (ctx : lexp_context) sl name t = let meta = Unif.create_metavar ctx sl t in mkMetavar (meta, S.identity, name) +(* Metavars can be instantiated/solved by instance resolution if their + context is saved. `newInstanceMetavar` creates a metavar and saves + its elab context for this purpose. This is a necessary, but not + sufficient condition: the metavar also needs to have a type that is + a class for resolution to happen. `newShiftedInstanceMetavar` does + the same as `newInstanceMetavar`, but for metavars whose context + does not include the variables in the current scope level (which + seems to be the case for explicit metavariables, currently). *) + +let newInstanceMetavar (ctx : elab_context) name t = + let lctx = ectx_to_lctx ctx in + let sl = ectx_to_scope_level ctx in + let meta = Unif.create_metavar lctx sl t in + Inst.save_metavar_resolution_ctxt meta ctx (fst name); + mkMetavar (meta, S.identity, name) + +let newShiftedInstanceMetavar (ctx : elab_context) name t = + let ctx_shift = ectx_local_scope_size ctx in + let octx = Myers.nthcdr ctx_shift (ectx_to_lctx ctx) in + let sl = ectx_to_scope_level ctx in + let subst = S.shift ctx_shift in + let (grm, (n, senv_map), _lctx, meta_scope, (tcs,inst_def,insts)) = ctx in + let new_n = n - ctx_shift in + let new_senv_map = SMap.filter (fun _ n' -> n' <= new_n) senv_map in + let new_tcctx = (tcs, inst_def, Myers.nthcdr ctx_shift insts) in + let nctx = (grm, (new_n, new_senv_map), octx, meta_scope, new_tcctx) in + let meta = Unif.create_metavar octx sl t in + Inst.save_metavar_resolution_ctxt meta nctx (fst name); + mkMetavar (meta, subst, name) + let newMetalevel (ctx : lexp_context) sl loc = newMetavar ctx sl (loc, Some "ℓ") type_level @@ -279,15 +321,15 @@ 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 _ot : elab_context = +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, a, b, c) = ctx in - (SMap.add name (level l, level r) grm, a, b, c) + let (grm, a, b, c, d) = ctx in + (SMap.add name (level l, level r) grm, a, b, c, d) | [o; _; _] -> sexp_error (sexp_location o) "Expecting a string"; ctx | _ @@ -545,6 +587,9 @@ let generalize (nctx : elab_context) e = wrap (IMap.mem id nes) vname mt' l e' in loop (IMap.empty) 0 mfvs +let wrapLambda ne vname t _l e = + mkLambda ((if ne then Aimplicit else Aerasable), vname, t, e) + let elab_p_id ((l,name) : symbol) : vname = (l, match name with "_" -> None | _ -> Some name) @@ -608,24 +653,49 @@ and elab_special_form ctx f args ot = -> lexp_error loc f "Unknown special-form: %s" (lexp_string f); sform_dummy_ret ctx loc -(* Make up an argument of type `t` when none is provided. *) -and get_implicit_arg ctx loc oname t = - newMetavar - (ectx_to_lctx ctx) - (ectx_to_scope_level ctx) - (loc, oname) - t +and elab_special_decl_form ctx f args = + let loc = lexp_location f in + match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with + | Builtin ((_, name), _) -> + (* Special form. *) + (get_special_decl_form name) ctx loc args + | _ -> lexp_error loc f "Unknown special-decl-form: %s" (lexp_string f); ctx (* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = let rec instantiate t args = match OL.lexp'_whnf t (ectx_to_lctx ctx) with | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) - -> let arg = get_implicit_arg ctx (lexp_location e) v t1 in - instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) + -> let arg = newInstanceMetavar ctx (lexp_location e, v) t1 in + instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) | _ -> (mkCall (e, List.rev args), t) in instantiate t [] +and resolve_instances e = + Inst.resolve_instances instantiate_implicit e + +and resolve_instances_and_generalize ctx e = + resolve_instances e; + generalize ctx e + +and sdform_typeclass (ctx : elab_context) (_l : location) sargs + : elab_context = + let make_typeclass ctx sarg = + let (t, _) = infer sarg ctx in + Inst.add_typeclass ctx t + in + List.fold_left make_typeclass ctx sargs + +and sdform_instance (inst : bool) (ctx : elab_context) (_l : location) sargs + : elab_context = + let make_instance ctx sarg = + let (lxp, _) = infer sarg ctx in + match lexp_lexp' lxp with + | Var (_, idx) -> ectx_set_inst ctx idx inst + | _ -> (lexp_error (lexp_location lxp) lxp + "Only variables can be instances"; ctx) in + List.fold_left make_instance ctx sargs + and infer_type pexp ectx var = (* We could also use lexp_check with an argument of the form * Sort (?s), but in most cases the metavar would be allocated @@ -926,15 +996,7 @@ and elab_macro_call ctx func args ot = | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) (lexp_location func) | Some t -> t in - let sxp = match lexp_expand_macro (lexp_location func) - func args ctx (Some t) with - | Vcommand cmd - -> (match cmd () with - | Vsexp (sxp) -> sxp - | v -> value_fatal (lexp_location func) v - "Macros should return a IO Sexp") - | v -> value_fatal (lexp_location func) v - "Macros should return an IO" in + let sxp = lexp_expand_macro (lexp_location func) func args ctx (Some t) in elaborate ctx sxp ot (* Identify Call Type and return processed call. *) @@ -977,13 +1039,10 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = (* Don't instantiate after the last explicit arg: the rest is done, * when needed in infer_and_check (via instantiate_implicit). *) when not (sargs = [] && SMap.is_empty pending) - -> let larg = get_implicit_arg - ctx (match sargs with - | [] -> loc - | sarg::_ -> sexp_location sarg) - v arg_type in - handle_fun_args ((ak, larg) :: largs) sargs pending - (L.mkSusp ret_type (S.substitute larg)) + -> let arg_loc = try sexp_location (List.hd sargs) with _ -> loc in + let larg = newInstanceMetavar ctx (arg_loc, v) arg_type in + handle_fun_args ((ak, larg) :: largs) sargs pending + (L.mkSusp ret_type (S.substitute larg)) | [], _ -> (if not (SMap.is_empty pending) then let pending = SMap.bindings pending in @@ -1025,7 +1084,7 @@ and lexp_parse_inductive ctors ctx = (fun (ak, n, t) aa -> mkArrow (ak, n, t, dummy_location, aa)) acc impossible in - let g = generalize nctx altacc in + let g = resolve_instances_and_generalize nctx altacc in let altacc' = g (fun _ne vname t l e -> mkArrow (Aerasable, vname, t, l, e)) altacc in @@ -1091,7 +1150,7 @@ and lexp_eval ectx e = raise exc and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) - : value_type = + : sexp = (* Build the function to be called *) let macro_expand = BI.get_predef "Macro_expand" ctx in @@ -1103,8 +1162,16 @@ and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) let args = [macro; BI.o2v_list sargs] in (* FIXME: Make a proper `Var`. *) - EV.eval_call loc (EL.Var ((DB.dloc, Some "expand_macro"), 0)) ([], []) - macro_expand args + let value = EV.eval_call loc (EL.Var ((DB.dloc, Some "expand_macro"), 0)) + ([], []) macro_expand args in + match value with + | Vcommand cmd + -> (match (cmd ()) with + | Vsexp (sexp) -> sexp + | _ -> fatal ~loc {|Macro "%s" should return an IO sexp|} + (lexp_string macro_funct)) + | _ -> fatal ~loc {|Macro "%s" should return an IO|} (lexp_string macro_funct) + (* Print each generated decls *) (* and sexp_decls_macro_print sxp_decls = @@ -1113,21 +1180,6 @@ and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) * List.iter (fun sxp -> sexp_decls_macro_print sxp) decls * | e -> sexp_print e; print_string "\n" *) -and lexp_decls_macro (loc, mname) sargs ctx: sexp = - try let lxp, _ltp = infer (Symbol (loc, mname)) ctx in - - (* FIXME: Check that (conv_p ltp Macro)! *) - let ret = lexp_expand_macro loc lxp sargs ctx None in - match ret with - | Vcommand cmd - -> (match cmd () with - | Vsexp (sexp) -> sexp - | _ -> fatal ~loc {|Macro "%s" should return an IO sexp|} mname) - | _ -> fatal ~loc {|Macro "%s" should return an IO|} mname - - with _e -> - fatal ~loc {|Macro "%s" not found|} mname - (* Elaborate a bunch of mutually-recursive definitions. * FIXME: Currently, we never apply generalization to recursive definitions, * which can leave "bogus" metavariables in the term (and it also means we @@ -1140,9 +1192,6 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) (* FIXME: Generalize when/where possible, so things like `map` can be defined without type annotations! *) (* Preserve the new operators added to nctx. *) - let ectx = let (_, a, b, c) = ectx in - let (grm, _, _, _) = nctx in - (grm, a, b, c) in let (declmap) = List.fold_right (fun ((l, vname), sexp) (map) -> @@ -1158,12 +1207,15 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) * mutually-recursive block would not have the * proper format, e.g. for `lctx_view`! *) let e = check sexp adjusted_t nctx in + resolve_instances e; (* let d = (v', LetDef (i + 1, e), t) in *) (IMap.add i ((l, Some vname), e, t) map) | _ -> Log.internal_error "Defining same slot!") defs (IMap.empty) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in - decls, ctx_define_rec ectx decls + let (_, a, b, c, _) = ctx_define_rec ectx decls in + let (grm, _, _, _, tcctx) = nctx in + decls, (grm, a, b, c, tcctx) and infer_and_generalize_type (ctx : elab_context) se name = let nctx = ectx_new_scope ctx in @@ -1197,7 +1249,7 @@ and infer_and_generalize_type (ctx : elab_context) se name = -> mkArrow (ak, v, t1, l, strip_rettype t2) | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) | _ -> t in - let g = generalize nctx (strip_rettype t) in + let g = resolve_instances_and_generalize nctx (strip_rettype t) in g (fun _ne name t l e -> mkArrow (Aerasable, name, t, l, e)) t @@ -1205,11 +1257,8 @@ and infer_and_generalize_type (ctx : elab_context) se name = and infer_and_generalize_def (ctx : elab_context) se = let nctx = ectx_new_scope ctx in let (e,t) = infer se nctx in - let g = generalize nctx e in - let e' = g (fun ne vname t _l e - -> mkLambda ((if ne then Aimplicit else Aerasable), - vname, t, e)) - e in + let g = resolve_instances_and_generalize nctx e in + let e' = g wrapLambda e in let t' = g (fun ne name t _l e -> mkArrow ((if ne then Aimplicit else Aerasable), name, t, sexp_location se, e)) @@ -1329,19 +1378,24 @@ and lexp_decls_1 ~loc {|Invalid definition syntax : "%s"|} (sexp_string thesexp); recur [] nctx pending_decls pending_defs) - | Some (Node (Symbol (l, "define-operator"), args)) - (* FIXME: Move this to a "special form"! *) - -> recur [] (sdform_define_operator nctx l args None) - pending_decls pending_defs - - | Some (Node (Symbol ((_l, _) as v), sargs)) - -> (* expand macro and get the generated declarations *) - let sdecl' = lexp_decls_macro v sargs nctx in - recur [sdecl'] nctx pending_decls pending_defs - | Some sexp - -> error ~loc:(sexp_location sexp) "Invalid declaration syntax"; + -> (* sdforms or macros *) + let sxp, sargs = match sexp with + | Node (sxp, sargs) -> sxp, sargs + | _ -> sexp, [] in + let lctx = ectx_to_lctx nctx in + let (f, t) = infer sxp nctx in + if (OL.conv_p lctx t type_special_form) then + recur [] (elab_special_decl_form nctx f sargs) pending_decls pending_defs + else if (OL.conv_p lctx t (BI.get_predef "Macro" nctx)) then + (* expand macro and get the generated declarations *) + let lxp, _ltp = infer sxp nctx in + let sdecl' = lexp_expand_macro (sexp_location sxp) lxp sargs nctx None in + 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 @@ -1526,7 +1580,7 @@ let sform_arrow kind ctx loc sargs _ot = let sform_immediate ctx loc sargs ot = match sargs with | [(String _) as se] -> mkImm (se), Inferred DB.type_string - | [(Integer _) as se] -> mkImm (se), Inferred DB.type_int + | [(Integer _) as se] -> mkImm (se), Inferred DB.type_integer | [(Float _) as se] -> mkImm (se), Inferred DB.type_float | [Block (_location, pts)] -> let grm = ectx_get_grammar ctx in @@ -1594,15 +1648,14 @@ let sform_identifier ctx loc sargs ot = | Some t (* `t` is defined in ctx instead of octx. *) -> Inverse_subst.apply_inv_subst t subst in - let mv = newMetavar octx sl (loc, Some name) t in + let mv = newShiftedInstanceMetavar ctx (loc, Some name) t in (if not (name = "") then let idx = match lexp_lexp' mv with | Metavar (idx, _, _) -> idx | _ -> fatal ~loc "newMetavar returned a non-Metavar" in rmmap := SMap.add name idx (!rmmap)); - (mkSusp mv subst, - match ot with Some _ -> Checked | None -> Lazy) + (mv, match ot with Some _ -> Checked | None -> Lazy) (* Normal identifier. *) | [Symbol id] -> elab_varref ctx id @@ -1874,6 +1927,15 @@ let register_special_forms () = (* FIXME: These should be functions! *) ("decltype", sform_decltype); ("declexpr", sform_declexpr); + ]; + List.iter add_special_decl_form + [ + ("define-operator", sdform_define_operator); + ("typeclass", sdform_typeclass); + ("instance", sdform_instance true); + ("not-instance", sdform_instance false); + ("bind-instances", (fun ctx _ _ -> ectx_set_inst_def ctx true)); + ("dont-bind-instances", (fun ctx _ _ -> ectx_set_inst_def ctx false)); ] (* Default context with builtin types @@ -1932,6 +1994,7 @@ let default_ectx builtin_size := get_size lctx; let ectx = dynamic_bind in_pervasive true (fun () -> read_file (btl_folder ^ "/pervasive.typer") lctx) in + let ectx = DB.ectx_set_inst_def ectx true in let _ = sform_default_ectx := ectx in ectx with e -> @@ -1952,7 +2015,9 @@ let lexp_expr_str str ctx = let source = new Source.source_string str in let pxps = sexp_parse_source source tenv grm limit in let lexps = lexp_parse_all pxps ctx in - List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) + List.iter (fun lxp -> + resolve_instances lxp; + ignore (OL.check (ectx_to_lctx ctx) lxp)) lexps; lexps ===================================== src/eval.ml ===================================== @@ -439,7 +439,7 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) match lxp with (* Leafs *) (* ---------------- *) - | Imm(Integer (_, i)) -> Vint (Z.to_int i) + | Imm(Integer (_, i)) -> Vinteger i | Imm(String (_, s)) -> Vstring s | Imm(Float (_, n)) -> Vfloat n | Imm(sxp) -> Vsexp sxp ===================================== src/instargs.ml ===================================== @@ -0,0 +1,238 @@ +(* Copyright (C) 2022 Free Software Foundation, Inc. + * + * Author: Jean-Alexandre Barszcz <jean-alexandre.barszcz(a)umontreal.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR + * A PARTICULAR PURPOSE. See the GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License along with + * this program. If not, see <http://www.gnu.org/licenses/>. *) + +module DB = Debruijn +module L = Lexp +module M = Myers +module OL = Opslexp +module S = Subst +module U = Util +module Unif = Unification + +open Printf + +(** If true, log all the matching instances when resolving. *) +let debug_list_all_candidates = ref false + +(** Optionnally limit resolution recursion depth. *) +let recursion_limit = ref (Some 100) + +(** Some variables may be skipped during instance resolution if + unification returns residual constraints (i.e. at this point during + inference, we do not have enough info to confirm or rule out a + match). If set to `some lvl`, log a message at level `lvl` when + that happens. *) +let log_skipped_uncertain_matches = ref (Some Log.Warning) + +let metavar_resolution_contexts = + ref (U.IMap.empty : (DB.elab_context * U.location) U.IMap.t) + +let lookup_metavar_resolution_ctxt (id : L.meta_id) + : (DB.elab_context * U.location) option + = U.IMap.find_opt id (!metavar_resolution_contexts) + +let save_metavar_resolution_ctxt (id : L.meta_id) ctx loc : unit + = (* First, check that there is only one possible resolution context + for any metavar. *) + (match U.IMap.find_opt id !metavar_resolution_contexts with + | Some (other_ctx, _) -> assert ((DB.get_size ctx) = (DB.get_size other_ctx)) + | _ -> ()); + metavar_resolution_contexts := + U.IMap.add id (ctx, loc) !metavar_resolution_contexts + +(** Check if a type is in the set of type class types. *) +let in_typeclass_set (ectx : DB.elab_context) (t : L.ltype) : bool = + let (_, _, _, _, (tcs, _, _)) = ectx in + let cl = DB.get_size ectx in + (* FIXME: We use go through a list element by element to check for + conversion, but syntactic equality of the heads (already in WHNF) + should be enough, probably? This means that we could use a real + set instead of a list! *) + List.exists (fun (t', cl') -> + let i = cl - cl' in + let t' = L.mkSusp t' (S.shift i) in + (* We could use unification to be more general, but conversion + on the heads of the calls seems simpler, faster, and good + enough. Also, we would need to undo instanciations after + unification. *) + OL.conv_p (DB.ectx_to_lctx ectx) t t' + ) tcs + +(** Get the head of a call. For instance, the call of `(Monoid α)` is + `Monoid`. *) +let get_head (lctx : DB.lexp_context) (t : L.ltype) : L.ltype = + let whnft = OL.lexp_whnf t lctx in + match L.lexp_lexp' whnft with + | L.Call (head, _) -> head + | _ -> whnft + +(** A type is a type class if its head is in the set of type class + types of the elaboration context. *) +let is_typeclass (ctx : DB.elab_context) (t : L.ltype) = + let head = get_head (DB.ectx_to_lctx ctx) t in + in_typeclass_set ctx head + +(** Add the type at the head of a call to the set of type class types + in the elaboration context. *) +let add_typeclass (ctx : DB.elab_context) (t : L.ltype) : DB.elab_context = + let head = get_head (DB.ectx_to_lctx ctx) t in + DB.ectx_add_typeclass ctx head + +(** The result type for matching.*) +type matching + = Impossible (* Unification (matching) failed with impossible constraints *) + | Possible (* Unification returned residual constraints: possible + match under the right metavariable associations. *) + | Match (* Perfect match: no constraints. *) + +let try_match t1 t2 lctx sl = + let has_impossible constraints = + List.exists (function | (Unif.CKimpossible,_,_,_) -> true + | _ -> false) + constraints in + match Unif.unify ~matching:sl t1 t2 lctx with + | [] -> Match + | constraints when has_impossible constraints -> Impossible + | _ -> Possible + +let myers_zip_filter_map_index (f : int -> 'a -> 'b -> 'c option) + (ma : 'a M.myers) (mb : 'b M.myers) : ('c M.myers) + = snd (M.fold_right2 + (fun x y (i, l') -> + match (f i x y) with + | Some r -> (i - 1, M.cons r l') + | None -> (i - 1, l')) + ma mb (M.length ma - 1, M.nil)) + +let myers_zip_sum_options (f : int -> 'a -> 'b -> 'c option) + (ma : 'a M.myers) (mb : 'b M.myers) : 'c option = + let rec loop i ma mb = + M.case ma + (fun () -> None) + (fun x xs -> + M.case mb + (fun () -> None) + (fun y ys -> + match f i x y with + | Some r -> Some r + | None -> loop (i + 1) xs ys)) in + loop 0 ma mb + +let search_instance (instantiate_implicit) (ctx : DB.elab_context) + (loc : U.location) (t : L.ltype) : L.lexp option = + Log.log_debug ~loc "Resolving type `%s`" (L.lexp_string t); + let lctx = DB.ectx_to_lctx ctx in + let (_, _, insts) = DB.ectx_to_tcctx ctx in + assert (M.length lctx = M.length insts); + + (* Increment the scope level and save it, as it is used to select + the instantiatable metavariables during matching. *) + let ctx = DB.ectx_new_scope ctx in + let sl = (DB.ectx_to_scope_level ctx) in + + (* For any env_elem in the context, if it's an instance, check if + its (implicitly applied) type is matching the type that we are + looking for, and return the applied expression (ex: `(nil (t := + Int))` for a `(List Int)`). The expression is tupled with the + index and env_elem, for convenience. *) + let env_elem_match (i : int) (elem : DB.env_elem) (is_inst : bool) + : (int * DB.env_elem * L.lexp) option = + if not is_inst then None else + let ((_, namopt), _, t') = elem in + let var = L.mkVar ((loc,namopt), i) in + let t' = L.mkSusp t' (S.shift (i + 1)) in + let (e, t') = instantiate_implicit var t' ctx in + (* All candidates should have a type that is a typeclass. *) + if not (is_typeclass ctx t') then None else + match try_match t t' lctx sl with + | Impossible -> None + | Possible -> + (match !log_skipped_uncertain_matches with + | Some level -> + Log.log_msg ignore level ~loc + "Skipping potential instance `%s : %s` while resolving for `%s`" + (L.lexp_string var) (L.lexp_string t') + (L.lexp_string t) + | None -> ()); + None + | Match -> Some (i, elem, e) in + + let inst = + if !debug_list_all_candidates then + let candidates = + myers_zip_filter_map_index env_elem_match lctx insts in + Log.log_debug "Candidates for instance of type `%s`:" (L.lexp_string t) + ~print_action:(fun () -> + M.iteri (fun _ (i, ((_, so),_,t'), _) -> + printf "%-4i %-10s %s\n" + i (* De Bruijn index *) + (match so with | Some s -> s | None -> "<none>") (* Var name *) + (L.lexp_string t') (* Variable type *) + ) candidates); + M.case candidates (fun _ -> None) (fun car _ -> Some car) + else myers_zip_sum_options env_elem_match lctx insts in + + match inst with + | None -> None + | Some (i, (vname, _, t'), e) -> + let t' = L.mkSusp t' (S.shift (i + 1)) in + Log.log_debug ~loc + "Found instance for `%s` at index %i: `%s : %s`" + (L.lexp_string t) i + (L.lexp_string (L.mkVar (vname, i))) (L.lexp_string t'); + Some e + +let resolve_instances instantiate_implicit e = + let rec resolve_instances e limit = + let (_, (fv_map, _)) = OL.fv e in + let strict_or = (||) in (* Remove short-circuiting *) + let changed = + U.IMap.fold (fun i (_sl, t, _cl, _vn) changed -> + strict_or changed + (match lookup_metavar_resolution_ctxt i with + | Some (ctx, loc) -> + (* Start by the instance metavars in the type: no need + to decrement the recursion limit here. *) + resolve_instances t limit; + let uninstantiated = + match L.metavar_lookup i with + | MVar _ -> true + | _ -> false in + if uninstantiated && is_typeclass ctx t then + (match search_instance instantiate_implicit ctx loc t with + | Some e -> Unif.associate i e; true + | None -> + (* The metavar will be generalized, unified, or + will remain and cause an error. *) + Log.log_info ~loc "No instance found for type `%s`" + (L.lexp_string t); false + ) + else false + | None -> false + )) fv_map false in + if changed then + match limit with + | Some l when l > 0 -> + resolve_instances e (Some (l - 1)) + | None -> resolve_instances e None + | _ -> + Log.log_error ~loc:(L.lexp_location e) + "Instance resolution recursion limit reached in expression : `%s`" + (L.lexp_string e) in + resolve_instances e !recursion_limit ===================================== src/myers.ml ===================================== @@ -138,9 +138,16 @@ let rec fold_right f l i = match l with | Mnil -> i | Mcons (x, l, _, _) -> f x (fold_right f l i) +let rec fold_right2 f l1 l2 i = + match l1, l2 with + | Mnil, _ -> i + | _, Mnil -> i + | Mcons (x, xs, _, _), + Mcons (y, ys, _, _) -> f x y (fold_right2 f xs ys i) + let map f l = fold_right (fun x l' -> cons (f x) l') l nil -let iteri f l = fold_left (fun i x -> f i x; i + 1) 0 l +let iteri f l = ignore (fold_left (fun i x -> f i x; i + 1) 0 l) let reverse (l : 'a myers) : 'a myers = fold_left (fun cdr car -> cons car cdr) nil l ===================================== src/opslexp.ml ===================================== @@ -633,7 +633,7 @@ and check'' erased ctx e = s in match lexp_lexp' e with | Imm (Float (_, _)) -> DB.type_float - | Imm (Integer (_, _)) -> DB.type_int + | Imm (Integer (_, _)) -> DB.type_integer | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> (log_tc_error ~loc:(lexp_location e) "Unsupported immediate value!"; @@ -1081,7 +1081,7 @@ and fv (e : lexp) : (DB.set * mv_set) = and get_type ctx e = match lexp_lexp' e with | Imm (Float (_, _)) -> DB.type_float - | Imm (Integer (_, _)) -> DB.type_int + | Imm (Integer (_, _)) -> DB.type_integer | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> DB.type_int | Builtin (_, t) -> t ===================================== src/unification.ml ===================================== @@ -443,7 +443,27 @@ and unify_call (matching : scope_level option) (call: lexp) (lxp: lexp) ctx vs (List.combine lxp_list1 lxp_list2) with Invalid_argument _ (* Lists of diff. length in combine. *) -> [(CKresidual, ctx, call, lxp)]) - | (_, _) -> [(CKresidual, ctx, call, lxp)] + | _ -> + let head_left = match lexp_lexp' call with + | Call (head_left, _) -> head_left + | _ -> call in + let head_right = match lexp_lexp' lxp with + | Call (head_right, _) -> head_right + | _ -> lxp in + let for_sure_irreducible_call_head ctx head = + match OL.lexp'_whnf head ctx with + | (Imm _ | Cons _ | Inductive _) -> true + | Builtin ((_, name), _) + -> not (SMap.mem name !Opslexp.reducible_builtins) + | _ -> false in + if for_sure_irreducible_call_head ctx head_left && + for_sure_irreducible_call_head ctx head_right && + not (OL.conv_p ctx head_left head_right) + then (* Whichever argument or substitution is applied, the + inconvertible heads will remain. *) + [(CKimpossible, ctx, head_left, head_right)] + else + [(CKresidual, ctx, call, lxp)] (** Unify a Case with a lexp - Case, Case -> try to unify ===================================== tests/dune ===================================== @@ -5,6 +5,7 @@ env_test eval_test gambit_test + instargs_test inverse_test lexp_test lexer_test ===================================== tests/elab_test.ml ===================================== @@ -52,7 +52,11 @@ let add_elab_test_decl = let _ = add_elab_test_expr "Instanciate implicit arguments" ~setup:{| -f : (i : Int) -> Eq i i -> Int; +%% FIXME: Unification not powerful enough to handle polymorphic ints +%% here... It seems that we would need unif. of Case or Proj. +typer-immediate = ##typer-immediate; + +f : (i : Integer) -> Eq i i -> Integer; f = lambda i -> lambda eq -> i; |} ~expected:"f 4 (Eq_refl (x := 4));" @@ -66,7 +70,7 @@ box = (datacons Box box); unbox b = ##case_ (b | box inside => inside); alwaysbool b = ##case_ (b | box _ => Bool); -example1 : unbox (box (lambda x -> Bool)) 1; +example1 : unbox (box (lambda x -> Bool)) (1 : Int); example1 = true; example2 : alwaysbool (box Int); @@ -82,10 +86,10 @@ box = (datacons Box box); unbox : (Box ?t) -> ?t; unbox b = b.inside; -example1 : unbox (box (lambda x -> Bool)) 1; +example1 : unbox (box (lambda x -> Bool)) (1 : Int); example1 = true; -example2 : Eq (__\.__ (box 1) inside) 1; +example2 : Eq (__\.__ (box 1) inside) (1 : Int); example2 = Eq_refl; |} @@ -148,7 +152,7 @@ let _ = add_elab_test_decl unify = macro ( lambda sxps -> - do {vname <- gensym (); + do IO {vname <- gensym (); IO_return (quote ((uquote vname) : (uquote (Sexp_node (Sexp_symbol "##Eq") sxps)); (uquote vname) = Eq_refl; ===================================== tests/eval_test.ml ===================================== @@ -54,14 +54,14 @@ let test_eval_eqv_named name decl run res = let test_eval_eqv decl run res = test_eval_eqv_named run decl run res -let _ = test_eval_eqv "" "2 + 2" "4" +let _ = test_eval_eqv "" "2 + 2" "(4 : Int)" let _ = test_eval_eqv_named "Variable Cascade" - "a = 10; b = a; c = b; d = c;" + "a = 10 : Int; b = a; c = b; d = c;" - "d" (* == *) "10" + "d" (* == *) "10 : Int" (* Let * ------------------------ *) @@ -72,17 +72,17 @@ let _ = test_eval_eqv_named "c = 3; e = 1; f = 2; d = 4;" "let a = -5; x = 50; y = 60; b = 20; - in a + b;" (* == *) "15" + in a + b;" (* == *) "15 : Int" let _ = test_eval_eqv_named "Let2" - "c = 3; e = 1; f = 2; d = 4;" + "c = 3 : Int; e = 1; f = 2; d = 4;" "let TrueProp = typecons TrueProp I; I = datacons TrueProp I; - x = let a = 1; b = 2 in I - in (case x | I => c);" (* == *) "3" + x = let a = 1 : Int; b = 2 : Int in I + in (case x | I => c);" (* == *) "3 : Int" let _ = test_eval_eqv_named "Let-erasable" @@ -90,7 +90,7 @@ let _ = test_eval_eqv_named "c = 3; e = 1; f = 2; d = 4;" "let id = lambda t ≡> lambda (x : t) -> x; - in (lambda t ≡> let t1 = t in id (t := t1)) 3" (* == *) "3" + in (lambda t ≡> let t1 = t in id (t := t1)) (3 : Int)" (* == *) "3 : Int" (* Lambda * ------------------------ *) @@ -101,7 +101,7 @@ let _ = test_eval_eqv_named "sqr : Int -> Int; sqr = lambda x -> x * x;" - "sqr 4;" (* == *) "16" + "sqr 4;" (* == *) "16 : Int" let _ = test_eval_eqv_named "Nested Lambda" @@ -112,7 +112,7 @@ let _ = test_eval_eqv_named cube : Int -> Int; cube = lambda x -> x * (sqr x);" - "cube 4" (* == *) "64" + "cube 4" (* == *) "64 : Int" (* Cases + Inductive types @@ -121,7 +121,8 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Inductive::Case" - "i = 90; + "typer-immediate = ##typer-immediate; + i = 90; idt : Type; idt = typecons (idtd) (ctr0) (ctr1 idt) (ctr2 idt) (ctr3 idt); d = 10; @@ -134,7 +135,7 @@ let _ = test_eval_eqv_named b = (ctr2 (ctr2 ctr0)); z = 3; c = (ctr3 (ctr2 ctr0)); w = 4; - test_fun : idt -> Int; + test_fun : idt -> Integer; test_fun = lambda k -> case k | ctr1 l => 1 | ctr2 l => 2 @@ -167,7 +168,7 @@ let _ = test_eval_eqv_named "to-num zero; to-num one; to-num two;" - "0; 1; 2" + "0 : Int; 1 : Int; 2 : Int" let _ = test_eval_eqv_named "Inductive::Nat Plus" @@ -186,7 +187,7 @@ let _ = test_eval_eqv_named to-num (plus two zero); to-num (plus two one);" - "2; 2; 3" + "2 : Int; 2 : Int; 3 : Int" let _ = test_eval_eqv_named "Mutually Recursive Definition" @@ -209,7 +210,7 @@ let _ = test_eval_eqv_named "odd one; even one; odd two; even two;" - "1; 0; 0; 1" + "1 : Int; 0 : Int; 0 : Int; 1 : Int" let _ = test_eval_eqv_named @@ -223,7 +224,7 @@ let _ = test_eval_eqv_named "inc1 1; inc2 2; inc1 3;" - "2; 3; 4" + "2 : Int; 3 : Int; 4 : Int" (* * Lists @@ -231,7 +232,7 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv_named "Lists" - "my_list = cons 1 + "my_list = cons (1 : Int) (cons 2 (cons 3 (cons 4 nil))); @@ -240,19 +241,19 @@ let _ = test_eval_eqv_named in L; cons' = datacons List' cons; nil' = datacons List' nil; - my_list' = (cons' 1 nil');" + my_list' = (cons' (1 : Int) nil');" "list.length my_list; list.head my_list; list.head (list.tail my_list)" - "4; some 1; some 2" + "4 : Int; some (1 : Int); some (2 : Int)" (* * Special forms *) -let _ = test_eval_eqv "w = 2" "decltype w" "Int" -let _ = test_eval_eqv "w = 2" "declexpr w" "2" +let _ = test_eval_eqv "w = (2 : Int)" "decltype w" "Int" +let _ = test_eval_eqv "w = (2 : Int)" "declexpr w" "2 : Int" let _ = (add_test "EVAL" "Monads" (fun () -> @@ -263,7 +264,7 @@ let _ = (add_test "EVAL" "Monads" (fun () -> let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - let rcode = "IO_run c 2" in + let rcode = "IO_run c (2 : Int)" in (* Eval defined lambda *) let ret = Elab.eval_expr_str rcode ectx rctx in @@ -284,7 +285,7 @@ let _ = test_eval_eqv_named fun (z := 1) (y := 2) (x := 3); fun (x := 3) (y := 2) (z := 1);" - "7; 13; 5; 7; 7" + "7 : Int; 13 : Int; 5 : Int; 7 : Int; 7 : Int" let _ = test_eval_eqv_named "Metavars" "f : ?; @@ -293,7 +294,7 @@ let _ = test_eval_eqv_named "Metavars" %inf x = inf (1 + x); test = 2;" - "1" "1" + "1 : Int" "1 : Int" let _ = test_eval_eqv_named "Explicit field patterns" @@ -310,7 +311,7 @@ let _ = test_eval_eqv_named case t | triplet (_ := af) (_ := bf) (d := df) cf => df; " - "\"hello\"; 5.0; \"hello\"; 5.0; \"hello\"; 7" + "\"hello\"; 5.0; \"hello\"; 5.0; \"hello\"; 7 : Int" let _ = test_eval_eqv_named "Implicit Arguments" @@ -325,7 +326,7 @@ let _ = test_eval_eqv_named fun (Eq_refl (x := 2)) |} - "2" + "2 : Int" let _ = test_eval_eqv_named "Equalities" @@ -335,7 +336,7 @@ let _ = test_eval_eqv_named Eq_cast (f := lambda v -> v) (p := p) x" "f Eq_refl 3" - "3" + "3 : Int" let _ = test_eval_eqv_named "Generic-typed case" @@ -350,7 +351,7 @@ let _ = test_eval_eqv_named Pair = typecons (Pair (a : Type) (b : Type)) (cons (x :: a) (y :: b)); - ptest : Pair Int String; + ptest : Pair Integer String; ptest = (##datacons Pair cons) (x := 4) (y := \"hello\"); px = case ptest | (##datacons ? cons) (x := v) => v; @@ -358,9 +359,9 @@ let _ = test_eval_eqv_named py = ptest.y;" "case tP - | (datacons ? true) (p := _) => 3 + | (datacons ? true) (p := _) => (3 : Integer) | (datacons ? false) (p := _) => 4; px; py" - "3; 4; \"hello\";" + "(3 : Integer); (4 : Integer); \"hello\";" let _ = test_eval_eqv_named "Y" @@ -374,14 +375,14 @@ let _ = test_eval_eqv_named | cons _ l => 1 + length l); |} - "length_y (cons 1 (cons 5 nil));" + "length_y (cons (1 : Int) (cons 5 nil));" - "2;" + "2 : Int;" let _ = test_eval_eqv_named "Block" - "a = 2" + "a = (2 : Int)" "a + 1;" "{a + 1};" @@ -396,8 +397,8 @@ let _ = test_eval_eqv_named IF_THEN_ELSE_ = if_then_else_; |} - "IF true THEN 2 ELSE 3;" - "if true then 2 else 3;" + "IF true THEN (2 : Int) ELSE 3;" + "if true then (2 : Int) else 3;" let _ = test_eval_eqv_named "Type Alias" "ListInt = List Int;" "" "" @@ -416,7 +417,7 @@ head ls p = | nil => unvoid (p (contra := (##DeBruijn 0))) | cons x xs => x); -l = (cons 0 nil); +l = (cons (0 : Int) nil); nil≠l : Not (Eq nil l); nil≠l = @@ -429,7 +430,7 @@ nil≠l = | cons _ _ => False) (); |} - "head l nil≠l" "0" + "head l nil≠l" "0 : Int" let _ = test_eval_eqv_named "Erasable cons args" @@ -480,4 +481,61 @@ let _ = if op = "/" && b = 0 then success else check_op op biop a b)))) +let _ = test_eval_eqv_named + "Instance arguments : head with proof" + {| +% We define the function `implicitly : ?t => ?t` to avoid the +% truncation of explicit metavar's (elab) context. Contexts are +% truncated to make inference easier in some cases, but only for +% explicit metavariables, not for automatically inserted +% metavars (ex: with a call to `implicitly`). These details might +% change... +implicitly = ?; + +exfalso (f : False) = ##case_ f; +Not p = (contra : p) ≡> False; +typeclass Eq; + +head : (ls : List ?τ) -> (p : Not (Eq nil ls)) -> ?τ; +head ls p = + case ls + | cons x xs => x + | nil => exfalso (p (contra := implicitly)); + |} + "" "" + +let _ = test_eval_eqv_named + "Instance arguments : boolean equality proofs" + {| +implicitly = ?; + +Eq_unerase = + lambda x y (p : Eq x y) ≡> + Eq_cast (p := p) (f := Eq x) Eq_refl; +exfalso (f : False) = ##case_ f; +Not p = (contra : p) ≡> False; +typeclass Eq; + +f : (b : Bool) -> (p : Not (Eq false b)) -> Eq true b; +f b p = + case b + | true => Eq_unerase (p := implicitly) + | false => exfalso (p (contra := implicitly)); + |} + "" "" + +let _ = test_eval_eqv_named + "Instance arguments : Coercible" + {| +type Coercible (from : Type) (to : Type) + | mkCoercible (from -> to); +typeclass Coercible; +coerce = lambda coercible => case coercible | mkCoercible coerce => coerce; + +intFromIntegerCoercion = mkCoercible (Integer->Int); + +example = (coerce ((Int->Integer 1) : Integer) : Int); + |} + "" "" + let _ = run_all () ===================================== tests/instargs_test.ml ===================================== @@ -0,0 +1,214 @@ +(* instargs_test.ml --- + * + * Copyright (C) 2016-2017 Free Software Foundation, Inc. + * + * Author: Jean-Alexandre Barszcz <jean-alexandre.barszcz(a)umontreal.ca> + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. + * + * -------------------------------------------------------------------------- *) + +open Typerlib +open Utest_lib + +module DB = Debruijn +module E = Elab +module I = Instargs +module L = Lexp +module O = Opslexp + +let add_test = add_test "INSTARGS" + +let default_ectx = E.default_ectx +let default_rctx = E.default_rctx +let dummy_vname = Util.dummy_location, None + +let make_metavar t ctx = + E.newInstanceMetavar ctx (Util.dummy_location, Some "inst") t + +let lexp_from_str str ctx = + List.hd (E.lexp_expr_str str ctx) + +(* Test the type class context : `is_typeclass` *) + +let _ = + let vars_str = + {| +a = 1; + +eq : Eq a (1 : Int); +eq = Eq_refl; + +typeclass Eq; + |} in + let ctx = snd (E.eval_decl_str vars_str default_ectx default_rctx) in + (List.map (fun (tstr, b) -> + let t = lexp_from_str tstr ctx in + add_test ("is_typeclass `" ^ tstr ^ "`") (fun _ -> + expect_equal_bool (I.is_typeclass ctx t) b + ) + ) [ + ("Int", false); + ("Eq", true); + ("decltype a", false); + ("decltype eq", true); + ]) + +(* Test the type class context : which vars are instances *) + +let _ = + let vars_str = + {| +% bind-instances; % This is the default. +a = 1; +b = 2; +not-instance b; +dont-bind-instances; +c = 3; +d = 4; +instance d; + |} in + let ctx = snd (E.eval_decl_str vars_str default_ectx default_rctx) in + let tcctx = DB.ectx_to_tcctx ctx in + let _,_,insts = tcctx in + (List.map (fun (lstr, b) -> + match L.lexp_lexp' (lexp_from_str lstr ctx) with + | L.Var (_,idx) -> + add_test ("is `" ^ lstr ^ "` an instance ?") (fun _ -> + expect_equal_bool (Myers.nth idx insts) b + ) + | _ -> failwith "Impossible" + ) [("a", true); ("b", false); ("c", false); ("d", true)]) + +(* Test : Make sure that we get the expected instance. + + Fill the context with instances of `Lift i` with `i` their de + Bruijn index, and resolve for various values of `i`. *) + +let lift_str = + {| +type Lift (l ::: TypeLevel) (t :: Type_ l) (x : t) + | mkLift; +typeclass Lift; + |} + +let lift_rctx, lift_ectx = + E.eval_decl_str lift_str default_ectx default_rctx + +let lift_n n ctx = + let str = Format.sprintf "mkLift (t := Int) (x := %i)" n in + lexp_from_str str ctx + +let lift_n_t n ctx = + let str = Format.sprintf "Lift (t := Int) (x := %i)" n in + lexp_from_str str ctx + +let rec extend_ectx_with_lifts n ectx = + let lift_n = lift_n n ectx in + let lift_n_t = O.get_type (DB.ectx_to_lctx ectx) lift_n in + let nctx = E.ctx_define ectx dummy_vname lift_n lift_n_t in + if n = 0 then nctx else + extend_ectx_with_lifts (n - 1) nctx + +let lifts_metavar i ctx = + make_metavar (lift_n_t i ctx) ctx + +let _ = + add_test "Matching the right instance" (fun _ -> + let depth = 100 in + let ectx = extend_ectx_with_lifts depth lift_ectx in + combine_results + (List.map (fun i -> + let lxp = lifts_metavar i ectx in + E.resolve_instances lxp; + expect_equal_lexp lxp (L.mkVar (dummy_vname, i)) + ) [0;1;2;4;13;17;58;99]) + ) + +(* Test : Recursive resolution builds the right calls. + + Use the singleton type for natural numbers to trigger recursive + searches. The resolution finds the instance `Ss'` for `SNat (S n)`, + and then recursively searches for `SNat n`, until it finds `Zs'` + for `SNat Z`. *) + +let snats_str = + {| +type Nat + | S Nat + | Z; + +type SNat (n : Nat) + | Ss (n-1 ::: Nat) (p ::: Eq (S n-1) n) (sn-1 :: SNat n-1) + | Zs (Z=n ::: Eq Z n); + +Ss' : (n : Nat) => SNat n => SNat (S n); +Ss' = lambda (n : Nat) => Ss (n := S n) (n-1 := n) (p := Eq_refl); + +Zs' : SNat Z; +Zs' = Zs (Z=n := Eq_refl); + +typeclass SNat; + |} + +let snats_rctx, snats_ectx = + Elab.eval_decl_str snats_str default_ectx default_rctx + +let to_nat n ctx = + let s = lexp_from_str "S" ctx in + let z = lexp_from_str "Z" ctx in + let rec loop i nat = + if i = 0 then nat else loop (i - 1) (L.mkCall (s,[Pexp.Anormal, nat])) in + loop n z + +let to_snat n ctx = + let s = lexp_from_str "S" ctx in + let ss = lexp_from_str "Ss'" ctx in + let zs = lexp_from_str "Zs'" ctx in + let rec loop i nat snat = + if i = 0 then snat else + loop (i - 1) + (L.mkCall (s,[Pexp.Anormal, nat])) + (L.mkCall (ss,[Pexp.Aimplicit, nat; Pexp.Aimplicit, snat])) in + loop n (to_nat 0 ctx) zs + +let snat_n_t n ctx = + let snat = lexp_from_str "SNat" ctx in + L.mkCall (snat, [Pexp.Anormal, to_nat n ctx]) + +let snat_metavar i ctx = + make_metavar (snat_n_t i ctx) ctx + +let _ = + add_test "Recursive resolution" (fun _ -> + let lctx = DB.ectx_to_lctx snats_ectx in + combine_results + (List.map (fun i -> + let lxp = snat_metavar i snats_ectx in + E.resolve_instances lxp; + expect_conv_lexp lctx lxp (to_snat i snats_ectx) + ) [0;1;2;4;13;17;58;99]) + ) + +let _ = + add_test "Resolution recursion limit" (fun _ -> + let limit = 20 in + Instargs.recursion_limit := Some limit; + let lxp = snat_metavar limit snats_ectx in + expect_throw L.lexp_string + (fun _ -> E.resolve_instances lxp; Log.stop_on_error (); lxp)) + +let _ = run_all () ===================================== tests/macro_test.ml ===================================== @@ -62,12 +62,12 @@ let _ = (add_test "MACROS" "macros decls" (fun () -> let chain-decl : Sexp -> Sexp -> Sexp; chain-decl a b = Sexp_node (Sexp_symbol \"_;_\") (cons a (cons b nil)) in - let make-decl : String -> Int -> Sexp; + let make-decl : String -> Sexp -> Sexp; make-decl name val = - (Sexp_node (Sexp_symbol \"_=_\") (cons (Sexp_symbol name) (cons (Sexp_integer (Int->Integer val)) nil))) in + (Sexp_node (Sexp_symbol \"_=_\") (cons (Sexp_symbol name) (cons val nil))) in - let d1 = make-decl \"a\" 1 in - let d2 = make-decl \"b\" 2 in + let d1 = make-decl \"a\" (quote (1 : Int)) in + let d2 = make-decl \"b\" (quote (2 : Int)) in IO_return (chain-decl d1 d2); my-decls = macro decls-impl; ===================================== tests/unify_test.ml ===================================== @@ -88,9 +88,12 @@ let _ = context (and not given a value) to make sure that they cannot be reduced. *) let _, ectx = Elab.lexp_decl_str - {| type Nat + {| + typer-immediate = ##typer-immediate; + type Nat | Z - | S (Nat); |} ectx in + | S (Nat); + |} ectx in let dloc = U.dummy_location in let nat = mkVar ((dloc, Some "Nat"), 2) in let shift l i = mkSusp l (S.shift i) in @@ -107,9 +110,9 @@ let _ = ("a", nat); ("b", nat)] in - add_unif_test_s "same integer" "4" "4" Equivalent; - add_unif_test_s "diff. integers" "3" "4" Nothing; - add_unif_test_s "int and builtin" "3" "##Int" Nothing; + add_unif_test_s "same integer" ~ectx "4" "4" Equivalent; + add_unif_test_s "diff. integers" ~ectx "3" "4" Nothing; + add_unif_test_s "int and builtin" ~ectx "3" "##Int" Nothing; add_unif_test_s "same var" ~ectx "a" "a" Equivalent; add_unif_test_s "diff. var" ~ectx "a" "b" Constraint; add_unif_test_s "var and integer" ~ectx "a" "1" Constraint; @@ -134,6 +137,11 @@ let _ = (* Not recursive! Refers to the previous def of Nat. *) Equivalent; + add_unif_test_s "calls to different constructors" ~ectx + "S (S Z)" "S Z" Nothing; + add_unif_test_s "calls to different constants" ~ectx + "Nat" "Eq (t := Nat) Z a" Nothing; + (* Metavariables *) add_unif_test_s "same metavar" "?m" "?m" Equivalent; add_unif_test_s "diff. metavar" "?m1" "?m2" Unification; @@ -147,7 +155,7 @@ let _ = {| a = 1; -eq : Eq a 1; +eq : Eq a (1 : Int); eq = Eq_refl; eq_any : (false : False) => (x : Int) => Eq a x; ===================================== tests/utest_lib.ml ===================================== @@ -41,6 +41,8 @@ type section = test_fun SMap.t * string list let success = 0 let failure = -1 +let combine_results = List.fold_left (+) 0 + (* * SECTION NAME - TEST NAME - FUNCTION (() -> int) * "Let" - "Base Case" - (fun () -> success ) @@ -127,11 +129,15 @@ let _expect_equal_t equality_test to_string value expect = let print_value_list values = List.fold_left (fun s v -> s ^ "\n" ^ Env.value_string v) "" values +let expect_equal_bool = _expect_equal_t Bool.equal string_of_bool let expect_equal_int = _expect_equal_t Int.equal string_of_int let expect_equal_float = _expect_equal_t Float.equal string_of_float let expect_equal_str = _expect_equal_t String.equal (fun g -> g) let expect_equal_values = _expect_equal_t Env.value_eq_list print_value_list +let expect_equal_lexp = _expect_equal_t Lexp.eq Lexp.lexp_string +let expect_conv_lexp ctx = _expect_equal_t (Opslexp.conv_p ctx) Lexp.lexp_string + let expect_equal_lexps = let rec lexp_list_eq l r = match l, r with @@ -182,6 +188,14 @@ let expect_equal_decls = in _expect_equal_t decl_list_eq string_of_decl_list +let expect_throw to_string test = + try let value = test () in + ut_string2 (red ^ "EXPECTED an exception" ^ reset ^ "\n"); + ut_string2 (red ^ "GOT: " ^ reset ^ "\n" ^ (to_string value) ^ "\n"); + failure + with + | _ -> success + (* USAGE * * (add_test "LET" "Base Case" (fun () -> View it on GitLab: https://gitlab.com/monnier/typer/-/compare/f2c2fcf1eda126cf2ec8df9169904aef… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/f2c2fcf1eda126cf2ec8df9169904aef… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][instance-args] 29 commits: Rewrite the Lexer module in terms of source objects.
by Jean-Alexandre Barszcz (＠jabarszcz) 24 Fév '22

24 Fév '22

Jean-Alexandre Barszcz pushed to branch instance-args at Stefan / Typer Commits: f289b62a by Simon Génier at 2021-05-29T12:12:42-04:00 Rewrite the Lexer module in terms of source objects. This might not look useful, but it will simplify a great deal our next change of add and end point to location records since all the location related code will be in there source objects. I ended up rewriting most of the Lexer. I tried to avoid doing that, but the offset handling code was so mixed up with the rest than that turned out to give worse code and a diff as unreadable. I'm pretty confident that that the changes are OK since we are still able to load pervasives.typer and I wrote a few tests for the trickier inner operators. - - - - - 8d9a2367 by Simon Génier at 2021-06-09T12:28:31-04:00 Merge branch 'lexer-with-source' - - - - - 4fb0ccd3 by Simon Génier at 2021-06-09T12:40:18-04:00 Shorten the names of a few methods on source objects. These names were redundants. For instance in `current_offset`, the `current` part is already hinted at by the fact that source objects are a kind of cursor. Overall I think the new names a clearer since they are more concise. - - - - - a7ac505a by Jean-Alexandre Barszcz at 2021-08-10T14:58:56-04:00 * src/elab.ml (elaborate): `check_inferred` when a type is given. Previously, `check_inferred` was mainly called from `check`, but some calls to `elaborate` play the same role as `check` (if an expected type is given), so we move this logic to `elaborate`. This allows implicit arguments to be instantiated in more places. For example, calls and variables are always inferred, but without `check_inferred`, the type provided to `elaborate` would be ignored. - - - - - aff91a51 by Simon Génier at 2021-09-28T17:16:11-04:00 Merge branch 'shorten-source-methods' - - - - - e8a59f86 by Simon Génier at 2021-09-28T17:25:19-04:00 Replace raw offsets with points which also track line and column. - - - - - 87882dea by Simon Génier at 2021-09-28T17:45:35-04:00 Compute location inside the source from the given point. - - - - - fce0fac4 by Simon Génier at 2021-09-28T18:16:00-04:00 Upgrade to OCaml 4.11. * Update the README * Remove a few functions that are now part of the standard library. - - - - - 01e6295a by Simon Génier at 2021-09-29T11:09:53-04:00 Remove doc strings from Typer. Doc strings are a good idea, but the implementation that was in Typer was not. They should not be hardcoded in the syntax of the langague, but rather a good implementation would use the metaprogramming capabilities of Typer to make them part of the standard library. - - - - - 8cfa2243 by Simon Génier at 2021-09-30T11:39:27-04:00 Locations now track their end points. - - - - - db1cf4da by Stefan Monnier at 2021-10-06T09:38:32-04:00 Merge remote-tracking branch 'gitlab/ocaml-4.11' into trunk - - - - - 8efdff37 by Stefan Monnier at 2021-10-06T10:01:02-04:00 Merge remote-tracking branch 'gitlab/purge-docstr' into trunk - - - - - 89cc2432 by Stefan Monnier at 2021-10-06T10:01:55-04:00 Merge remote-tracking branch 'gitlab/source-spans-2' into trunk - - - - - f832b339 by Simon Génier at 2021-10-28T10:43:05-04:00 Remove artisanal formatting functions in favour of printf. - - - - - 7f6f32dd by Simon Génier at 2021-10-28T10:43:38-04:00 Printfify log functions. - - - - - edf888bc by Simon Génier at 2021-10-28T11:00:18-04:00 Typer accepts subcommands (repl, compile, run) like git. This will hopefully simplify option handling as I add more modes of operation with their own option for running Typer code in a Gambit subprocess. - - - - - d3daf0a3 by Soilih BEN SOILIH at 2022-02-16T10:07:07-05:00 Add a `Proj` constructor to the `lexp` type We add a projection constructor to the Lexp type in order to be able to offer the completion in a satisfactory manner for the LSP server. When we write MODULE.FIELD, if FIELD doesn't exist, we could not offer the completion because the AST could not be generated at all. So we add this case to be able to have an AST and be able to find the functions of a module, and also select specific functions thanks to the label of a projection. * src/lexp.ml (lexp): Add `Proj` constructor. (lexp'_hash, lexp_head, lexp_location, push_susp, clean, lexp_unparse) (lexp_str): Adjust accordingly. (mkProj): new function. * src/elab.ml (adjust_subst.loop): Add `Proj` case for the loop substitution. (sform_proj): new special form. (register_special_forms): Register it. * src/opslexp.ml (pos_of_label): new function. (check'', get_type, fv, erase_type): * src/positivity.ml (positive'): Add new case for `Proj`. * src/eval.ml (eval): * src/apply_inv_subst.ml (apply_inv_subst): * src/elexp.ml (elexp, elexp_location, elexp_name, elexp_string): Add new case for `Proj`. * btl/pervasive.typer (__/.__): Delete macro. - - - - - 537ab8c3 by Jean-Alexandre Barszcz at 2022-02-16T13:49:48-05:00 * shell.nix : Set the Ocaml version to 4.11 - - - - - f89ed276 by Jean-Alexandre Barszcz at 2022-02-24T16:01:43-05:00 * src/opslexp.ml (lexp_whnf_aux): Add WHNF of Proj. - - - - - ee155042 by Jean-Alexandre Barszcz at 2022-02-24T16:05:35-05:00 * src/unification.ml (unify): Provide a `matching` mode. This new mode is for instance argument resolution, where unification is limited to a subset of the metavariables. We will characterize this subset with an increased scope level. (associate): Make `associate` mutate the global metavar table to provide a cleaner interface. - - - - - 649c82f3 by Jean-Alexandre Barszcz at 2022-02-24T16:10:43-05:00 * src/elab.ml: Handle sdforms in a common way. - - - - - cd1735cd by Jean-Alexandre Barszcz at 2022-02-24T16:19:18-05:00 * src/debruijn.ml: Add a type class context to the elab context. * src/elab.ml: Add the `typeclass` sdform that adds a type to the set of typeclasses in the typeclass context. Add the `instance` and `not-instance` sdforms that set the instance flag for given variables in the typeclass context. Add the `bind-instances` and `dont-bind-instances` sdforms that set the default instance flag for new variables. * src/instargs.ml: New source file for things related to instance arguments. - - - - - ef4cb013 by Jean-Alexandre Barszcz at 2022-02-24T16:20:04-05:00 * tests/instargs_test.ml: New file, test the type class context. - - - - - 51e2c2f1 by Jean-Alexandre Barszcz at 2022-02-24T16:29:35-05:00 * src/elab.ml: Save metavars' elaboration contexts for resolution. * src/instargs.ml: Keep a table of resolution contexts for instance metavariables. - - - - - fbcb99f4 by Jean-Alexandre Barszcz at 2022-02-24T16:40:23-05:00 * src/instargs: Implement instance resolution. * src/elab.ml: Resolve instances before every generalization. (lexp_check_decls): Resolve instances for recursive definitions. (lexp_expr_str): Resolve instances when elaborating from a string. * src/REPL.ml: Resolve and generalize expressions in the REPL. - - - - - 811bb343 by Jean-Alexandre Barszcz at 2022-02-24T16:43:00-05:00 * src/unification.ml (unify_call) : Return CKImpossible when we can. - - - - - 17cb9524 by Jean-Alexandre Barszcz at 2022-02-24T17:02:11-05:00 Make integer literals polymorphic using type classes * btl/poly-lits.typer: New file implementing polymorphic integer literals through the "typer-immediate" hook and type classes. * btl/pervasive.typer: Use the new definition of "typer-immediate". - - - - - f76b9510 by Jean-Alexandre Barszcz at 2022-02-24T17:02:20-05:00 Change integer literals to have type Integer by default - - - - - f2c2fcf1 by Jean-Alexandre Barszcz at 2022-02-24T17:48:16-05:00 Make `do` polymorphic with a `Monad` class. - - - - - 30 changed files: - README.md - btl/builtins.typer - btl/case.typer - btl/do.typer - + btl/monads.typer - btl/pervasive.typer - + btl/poly-lits.typer - debug_util.ml - + samples/nats.typer - shell.nix - src/REPL.ml - src/backend.ml - src/builtin.ml - src/debruijn.ml - src/debug.ml - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - − src/float.ml - src/fmt.ml - src/gambit.ml - src/heap.ml - + src/instargs.ml - − src/int.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml - src/listx.ml - src/log.ml The diff was not included because it is too large. View it on GitLab: https://gitlab.com/monnier/typer/-/compare/af2e4d1e180d93145e77d96df87588a2… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/af2e4d1e180d93145e77d96df87588a2… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][macro-expansion-tracing] Add a flag to show macros, their arguments and the expanded code.
by Simon Génier (＠ilovemonoids) 16 Fév '22

16 Fév '22

Simon Génier pushed to branch macro-expansion-tracing at Stefan / Typer Commits: 29c8aded by Simon Génier at 2022-02-16T19:17:56-05:00 Add a flag to show macros, their arguments and the expanded code. - - - - - 3 changed files: - src/elab.ml - src/log.ml - typer.ml Changes: ===================================== src/elab.ml ===================================== @@ -97,6 +97,9 @@ let lexp_fatal loc lexp = let value_fatal loc value = fatal ~loc ~print_action:(value_print_details value) +let macro_tracing_enabled = ref false +let trace_macro ~location fmt = Log.log_debug ~loc:location ~section:"MACRO" fmt + (** Type info returned by elaboration. *) type sform_type = | Checked (* Checked that the expression has the requested type. *) @@ -920,21 +923,39 @@ and check_case rtype (loc, target, ppatterns) ctx = mkCase (loc, tlxp, rtype, lpattern, dflt) -and elab_macro_call ctx func args ot = - let t - = match ot with - | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) - (lexp_location func) - | Some t -> t in - let sxp = match lexp_expand_macro (lexp_location func) - func args ctx (Some t) with +and elab_macro_call + (ctx : elab_context) + (func : lexp) + (args : token list) + (ot : ltype option) + : lexp * sform_type = + + let location = lexp_location func in + let t = + match ot with + | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) location + | Some t -> t + in + + if !macro_tracing_enabled + then + (trace_macro ~location {|expanding: %s|} (lexp_string func); + List.iteri + (fun i arg -> + arg |> sexp_string |> trace_macro ~location {|input %d: %s|} i) + args); + + let sxp = + match lexp_expand_macro location func args ctx (Some t) with | Vcommand cmd -> (match cmd () with - | Vsexp (sxp) -> sxp - | v -> value_fatal (lexp_location func) v - "Macros should return a IO Sexp") - | v -> value_fatal (lexp_location func) v - "Macros should return an IO" in + | Vsexp (sxp) -> sxp + | v -> value_fatal location v "Macros should return a IO Sexp") + | v -> value_fatal location v "Macros should return an IO" + in + if !macro_tracing_enabled + then trace_macro ~location {|output: %s|} (sexp_string sxp); + elaborate ctx sxp ot (* Identify Call Type and return processed call. *) ===================================== src/log.ml ===================================== @@ -114,15 +114,15 @@ let maybe_color_string color_opt str = | None -> str let string_of_log_entry {level; kind; section; loc; msg; _} = - let color = if typer_log_config.color then (level_color level) else None in + let color = if typer_log_config.color then level_color level else None in + let kind_string = Option.value ~default:(string_of_level level) kind in let parens s = "(" ^ s ^ ")" in - (Option.value ~default:"" (Option.map Source.Location.to_string loc) - ^ maybe_color_string - color - (Option.value ~default:(string_of_level level) kind) - ^ ":" - ^ Option.value ~default:"" (Option.map parens section) ^ " " - ^ msg) + sprintf + "%s %s:%s %s" + (Option.value ~default:"" (Option.map Source.Location.to_string loc)) + (maybe_color_string color kind_string) + (Option.value ~default:"" (Option.map parens section)) + msg let print_entry entry = print_endline (string_of_log_entry entry); ===================================== typer.ml ===================================== @@ -40,12 +40,22 @@ let arg_defs = ("-Vfull-lctx", Arg.Set Debruijn.log_full_lctx, - "Print the full lexp context on error."); + "Print the full lexp context on error"); + + ("-Vmacro-expansion", + Arg.Set Elab.macro_tracing_enabled, + "Trace macro expansion"); ] +let parse_args argv usage = + try Arg.parse_argv argv arg_defs add_input_file usage with + | Arg.Help (message) -> + print_string message; + exit 0 + let compile_main argv = let usage = Sys.executable_name ^ " compile [options] <file> …" in - Arg.parse_argv argv arg_defs add_input_file usage; + parse_args argv usage; let ectx = Elab.default_ectx in let backend = new Gambit.gambit_compiler (ectx_to_lctx ectx) stdout in @@ -57,7 +67,7 @@ let compile_main argv = let repl_main argv = let usage = Sys.executable_name ^ " repl [options] [<file>] …" in - Arg.parse_argv argv arg_defs add_input_file usage; + parse_args argv usage; print_string (Fmt.make_title " TYPER REPL "); print_endline " Typer 0.0.0 - Interpreter - (c) 2016-2021"; @@ -80,7 +90,7 @@ let repl_main argv = let run_main argv = let usage = Sys.executable_name ^ " run [options] <file> …" in - Arg.parse_argv argv arg_defs add_input_file usage; + parse_args argv usage; let ectx = Elab.default_ectx in let backend = new Eval.ast_interpreter (ectx_to_lctx ectx) in View it on GitLab: https://gitlab.com/monnier/typer/-/commit/29c8adedee2eef35b4fcc775d871bb9f5… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/29c8adedee2eef35b4fcc775d871bb9f5… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][macro-expansion-tracing] 2 commits: Add a `Proj` constructor to the `lexp` type
by Simon Génier (＠ilovemonoids) 16 Fév '22

16 Fév '22

Simon Génier pushed to branch macro-expansion-tracing at Stefan / Typer Commits: d3daf0a3 by Soilih BEN SOILIH at 2022-02-16T10:07:07-05:00 Add a `Proj` constructor to the `lexp` type We add a projection constructor to the Lexp type in order to be able to offer the completion in a satisfactory manner for the LSP server. When we write MODULE.FIELD, if FIELD doesn't exist, we could not offer the completion because the AST could not be generated at all. So we add this case to be able to have an AST and be able to find the functions of a module, and also select specific functions thanks to the label of a projection. * src/lexp.ml (lexp): Add `Proj` constructor. (lexp'_hash, lexp_head, lexp_location, push_susp, clean, lexp_unparse) (lexp_str): Adjust accordingly. (mkProj): new function. * src/elab.ml (adjust_subst.loop): Add `Proj` case for the loop substitution. (sform_proj): new special form. (register_special_forms): Register it. * src/opslexp.ml (pos_of_label): new function. (check'', get_type, fv, erase_type): * src/positivity.ml (positive'): Add new case for `Proj`. * src/eval.ml (eval): * src/apply_inv_subst.ml (apply_inv_subst): * src/elexp.ml (elexp, elexp_location, elexp_name, elexp_string): Add new case for `Proj`. * btl/pervasive.typer (__/.__): Delete macro. - - - - - feda20f6 by Simon Génier at 2022-02-16T19:08:10-05:00 Add a flag to show macros, their arguments and the expanded code. - - - - - 11 changed files: - btl/pervasive.typer - src/elab.ml - src/elexp.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/log.ml - src/opslexp.ml - src/positivity.ml - src/unification.ml - typer.ml Changes: ===================================== btl/pervasive.typer ===================================== @@ -1,6 +1,6 @@ %%% pervasive --- Always available definitions -%% Copyright (C) 2011-2020 Free Software Foundation, Inc. +%% Copyright (C) 2011-2022 Free Software Foundation, Inc. %% %% Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> %% Keywords: languages, lisp, dependent types. @@ -426,32 +426,6 @@ BoolMod = (##datacons Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); pair = datacons Pair pair; -__\.__ = - let mksel o f = - let constructor = Sexp_node (Sexp_symbol "##datacons") - (cons (Sexp_symbol "?") - (cons (Sexp_symbol "cons") - nil)); - pattern = Sexp_node constructor - (cons (Sexp_node (Sexp_symbol "_:=_") - (cons f (cons (Sexp_symbol "v") - nil))) - nil); - branch = Sexp_node (Sexp_symbol "_=>_") - (cons pattern (cons (Sexp_symbol "v") nil)); - in Sexp_node (Sexp_symbol "case_") - (cons (Sexp_node (Sexp_symbol "_|_") - (cons o (cons branch nil))) - nil) - in macro (lambda args - -> IO_return - case args - | cons o tail - => (case tail - | cons f _ => mksel o f - | nil => Sexp_error) - | nil => Sexp_error); - %% Triplet (tuple with 3 values) type Triplet (a : Type) (b : Type) (c : Type) | triplet (x : a) (y : b) (z : c); ===================================== src/elab.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2021 Free Software Foundation, Inc. + * Copyright (C) 2011-2022 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -97,6 +97,12 @@ let lexp_fatal loc lexp = let value_fatal loc value = fatal ~loc ~print_action:(value_print_details value) +let macro_tracing_enabled = ref false +let trace_macro location fmt = + if !macro_tracing_enabled + then Log.log_debug ~loc:location ~section:"MACRO" fmt + else Printf.ifprintf () fmt + (** Type info returned by elaboration. *) type sform_type = | Checked (* Checked that the expression has the requested type. *) @@ -429,6 +435,7 @@ let meta_to_var ids (e : lexp) = | Sort (_, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e | Var (n,i) -> if i < o then e else mkVar (n, i + count) + | Proj (l, lxp, lbl) -> mkProj (l, loop o lxp, lbl) | Susp (e, s) -> loop o (push_susp e s) | Let (l, defs, e) -> let len = List.length defs in @@ -919,21 +926,34 @@ and check_case rtype (loc, target, ppatterns) ctx = mkCase (loc, tlxp, rtype, lpattern, dflt) -and elab_macro_call ctx func args ot = - let t - = match ot with - | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) - (lexp_location func) - | Some t -> t in - let sxp = match lexp_expand_macro (lexp_location func) - func args ctx (Some t) with +and elab_macro_call + (ctx : elab_context) + (func : lexp) + (args : token list) + (ot : ltype option) + : lexp * sform_type = + + let location = lexp_location func in + let t = + match ot with + | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) location + | Some t -> t + in + + trace_macro location {|expanding: %s|} (lexp_string func); + List.iteri + (fun i arg -> arg |> sexp_string |> trace_macro location {|input %d: %s|} i) + args; + let sxp = + match lexp_expand_macro location func args ctx (Some t) with | Vcommand cmd -> (match cmd () with - | Vsexp (sxp) -> sxp - | v -> value_fatal (lexp_location func) v - "Macros should return a IO Sexp") - | v -> value_fatal (lexp_location func) v - "Macros should return an IO" in + | Vsexp (sxp) -> sxp + | v -> value_fatal location v "Macros should return a IO Sexp") + | v -> value_fatal location v "Macros should return an IO" + in + trace_macro location {|output: %s|} (sexp_string sxp); + elaborate ctx sxp ot (* Identify Call Type and return processed call. *) @@ -1726,6 +1746,18 @@ let sform_letin ctx loc sargs ot = match sargs with | _ -> sexp_error loc "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc +let sform_proj ctx loc sargs _ = + match sargs with + | [lxp;(Symbol (loca,str))] + -> let (ret,_) = infer lxp ctx in + let e = mkProj (loc,ret,(loca,str)) in + (e, Lazy) + | [_;_] + -> sexp_error loc "Second argument is not a Symbol!"; + sform_dummy_ret ctx loc + | _ -> sexp_error loc "Wrong arg number!"; + sform_dummy_ret ctx loc + let rec infer_level ctx se : lexp = match se with | Symbol (_, "z") -> mkSortLevel SLz @@ -1846,6 +1878,7 @@ let register_special_forms () = ("datacons", sform_datacons); ("typecons", sform_typecons); ("_:_", sform_hastype); + ("__.__", sform_proj); ("lambda_->_", sform_lambda Anormal); ("lambda_=>_", sform_lambda Aimplicit); ("lambda_≡>_", sform_lambda Aerasable); @@ -1855,7 +1888,7 @@ let register_special_forms () = ("case_", sform_case); ("let_in_", sform_letin); ("Type_", sform_type); - ("load", sform_load); + ("load", sform_load); (* FIXME: We should add here `let_in_`, `case_`, etc... *) (* FIXME: These should be functions! *) ("decltype", sform_decltype); ===================================== src/elexp.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2020 Free Software Foundation, Inc. + * Copyright (C) 2011-2022 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -52,6 +52,8 @@ type elexp = (* A variable reference, using deBruijn indexing. *) | Var of vref + | Proj of U.location * elexp * int + (* Recursive `let` binding. *) | Let of U.location * (vname * elexp) list * elexp @@ -83,6 +85,7 @@ let rec elexp_location e = match e with | Imm s -> sexp_location s | Var ((l,_), _) -> l + | Proj (l,_,_) -> l | Builtin ((l, _)) -> l | Let (l,_,_) -> l | Lambda ((l,_),_) -> l @@ -96,6 +99,7 @@ let elexp_name e = match e with | Imm _ -> "Imm" | Var _ -> "Var" + | Proj _ -> "Proj" | Let _ -> "Let" | Call _ -> "Call" | Cons _ -> "Cons" @@ -136,6 +140,8 @@ and elexp_string lxp = | Imm(s) -> sexp_string s | Builtin((_, s)) -> s | Var((_, s), i) -> L.maybename s ^ "[" ^ string_of_int i ^ "]" + | Proj (_,lxp,i) + -> "( __.__ " ^ elexp_string lxp ^ " " ^ (string_of_int i) ^ " )" | Cons (_, (_, s)) -> "datacons(" ^ s ^")" | Lambda((_, s), b) -> "lambda " ^ L.maybename s ^ " -> " ^ (elexp_string b) ===================================== src/eval.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018, 2020, 2021 Free Software Foundation, Inc. + * Copyright (C) 2011-2018, 2020, 2021, 2022 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -462,7 +462,12 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) -> eval_call (elexp_location f) f trace (eval f ctx trace) (List.map (fun e -> eval e ctx trace) args) - + (* Proj *) + | Proj (loc, e, i) + -> (match eval' e ctx with + | Vcons (_, vtl) -> List.nth vtl i + | _ -> error loc "Proj on a non-datatype constructor: %s \n" + (elexp_string e)) (* Case *) | Case (loc, target, pat, dflt) -> (eval_case ctx trace loc target pat dflt) ===================================== src/inverse_subst.ml ===================================== @@ -1,6 +1,6 @@ (* inverse_subst.ml --- Computing the inverse of a substitution -Copyright (C) 2016-2020 Free Software Foundation, Inc. +Copyright (C) 2016-2022 Free Software Foundation, Inc. Author: Vincent Bonnevalle <tiv.crb(a)gmail.com> @@ -264,6 +264,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = | Sort (_l, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) + | Proj (l,lxp,lbl) -> mkProj (l, apply_inv_subst lxp s, lbl) | Susp (e, s') -> apply_inv_subst (push_susp e s') s | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in ===================================== src/lexp.ml ===================================== @@ -1,6 +1,6 @@ (* lexp.ml --- Lambda-expressions: the core language. -Copyright (C) 2011-2021 Free Software Foundation, Inc. +Copyright (C) 2011-2022 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> Keywords: languages, lisp, dependent types. @@ -66,6 +66,7 @@ type ltype = lexp | Sort of U.location * sort | Builtin of symbol * ltype | Var of vref + | Proj of U.location * lexp * label | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of U.location * (vname * lexp * ltype) list * lexp @@ -245,6 +246,10 @@ let lexp'_hash (lp : lexp') = args))) | Susp (lp, subst) -> U.combine_hash 14 (U.combine_hash (lexp_hash lp) (Hashtbl.hash subst)) + | Proj (l,lxp,lbl) + -> U.combine_hash 15 (U.combine_hash (Hashtbl.hash l) + (U.combine_hash (Hashtbl.hash lxp) + (Hashtbl.hash lbl))) (* Equality function for hash table * using physical equality for "sub-lexp" and compare for `subst`. *) @@ -307,8 +312,9 @@ let hc (l : lexp') : lexp = let mkImm s = hc (Imm s) let mkSortLevel l = hc (SortLevel l) let mkSort (l, s) = hc (Sort (l, s)) -let mkBuiltin (v, t) = hc (Builtin (v, t)) +let mkBuiltin (v, t) = hc (Builtin (v, t)) let mkVar v = hc (Var v) +let mkProj (l,lxp,lbl) = hc (Proj (l,lxp,lbl)) let mkLet (l, ds, e) = hc (Let (l, ds, e)) let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) @@ -329,6 +335,7 @@ let lexp_head e = | Imm s -> if e = impossible then "impossible" else "Imm" ^ sexp_string s | Var _ -> "Var" + | Proj _ -> "Proj" | Let _ -> "let" | Arrow _ -> "Arrow" | Lambda _ -> "lambda" @@ -524,6 +531,7 @@ let rec lexp_location e = | Susp (e, _) -> lexp_location e (* | Susp (_, e) -> lexp_location e *) | Metavar (_,_,(l,_)) -> l + | Proj (l,_,_) -> l (********* Normalizing a term *********) @@ -590,6 +598,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) * in many other cases than just when we bump into a Susp. *) | Susp (e,s') -> push_susp e (scompose s' s) | (Var _ | Metavar _) -> nosusp (mkSusp e s) + | Proj (l,lxp,lbl) -> mkProj (l, mkSusp lxp s, lbl) and nosusp e = (* Return `e` with no outermost `Susp`. *) match lexp_lexp' e with @@ -653,6 +662,7 @@ let clean e = | Susp (e, s') -> clean (scompose s' s) e | Var _ -> if S.identity_p s then e else clean S.identity (mkSusp e s) + | Proj (l, lxp, lbl) -> mkProj (l, clean s lxp, lbl) | Metavar (idx, s', name) -> let s = scompose s' s in match metavar_lookup idx with @@ -671,6 +681,9 @@ let rec lexp_unparse lxp = | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) | Var ((loc, name), _) -> Symbol (loc, maybename name) + | Proj (l,lxp,(loc,str) ) + -> Node (Symbol (l, "__.__"), + [(lexp_unparse lxp);(Symbol (loc,str))]) | Cons (t, (l, name)) -> Node (sdatacons, [lexp_unparse t; Symbol (l, name)]) @@ -973,6 +986,9 @@ and lexp_str ctx (exp : lexp) : string = | Var ((_loc, name), idx) -> maybename name ^ (index idx) ; + | Proj (_, lxp, (_, str)) + -> "( __.__ " ^ lexp_str' lxp ^ " " ^ str ^ " )" + | Metavar (idx, subst, (_loc, name)) (* print metavar result if any *) -> (match metavar_lookup idx with ===================================== src/log.ml ===================================== @@ -114,15 +114,15 @@ let maybe_color_string color_opt str = | None -> str let string_of_log_entry {level; kind; section; loc; msg; _} = - let color = if typer_log_config.color then (level_color level) else None in + let color = if typer_log_config.color then level_color level else None in + let kind_string = Option.value ~default:(string_of_level level) kind in let parens s = "(" ^ s ^ ")" in - (Option.value ~default:"" (Option.map Source.Location.to_string loc) - ^ maybe_color_string - color - (Option.value ~default:(string_of_level level) kind) - ^ ":" - ^ Option.value ~default:"" (Option.map parens section) ^ " " - ^ msg) + sprintf + "%s %s:%s %s" + (Option.value ~default:"" (Option.map Source.Location.to_string loc)) + (maybe_color_string color kind_string) + (Option.value ~default:"" (Option.map parens section)) + msg let print_entry entry = print_endline (string_of_log_entry entry); ===================================== src/opslexp.ml ===================================== @@ -1,6 +1,6 @@ (* opslexp.ml --- Operations on Lexps -Copyright (C) 2011-2021 Free Software Foundation, Inc. +Copyright (C) 2011-2022 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> Keywords: languages, lisp, dependent types. @@ -747,6 +747,51 @@ and check'' erased ctx e = args) in let tct = arg_loop ctx erased args in tct + | Proj (l, e, (loc, label)) + -> ( let call_split e = + match lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + let etype = lexp_whnf (check erased ctx e) ctx in + let it, aargs = call_split etype in + match lexp'_whnf it ctx, aargs with + | Inductive (_, _, fargs, constructors), aargs + when SMap.cardinal constructors = 1 + -> let rec mksubst s fargs aargs = + match fargs, aargs with + | [], [] -> s + | _farg::fargs, (_ak, aarg)::aargs + -> mksubst (S.cons aarg s) fargs aargs + | _,_ -> (log_tc_error ~loc:l + "Wrong arg number to inductive type!"; s) in + let s = mksubst S.identity fargs aargs in + let (_,fieldtypes) = List.hd (SMap.bindings constructors) in + let rec getfieldtype s (fieldtypes + : (arg_kind * vname * ltype) list) = + match fieldtypes with + | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; + etype + | (ak, (_, Some fn), ftype)::_ when fn = label + (* We found our field! *) + -> if not (ak = Aerasable) + then mkSusp ftype s (* Yay! We found our field! *) + else (log_tc_error ~loc:l "Can't Proj an erasable field: %s" + label; + Lexp.impossible) + | (_, vdef, _)::fieldtypes + -> let fvdef vdef e loc lbl = + match vdef with + |(_, Some _) -> mkProj (loc, e, lbl) + |_ -> Lexp.impossible in + let fieldref = fvdef vdef e l (loc, label) in + getfieldtype (S.cons fieldref s) fieldtypes in + getfieldtype s fieldtypes + | Inductive _, _ + -> Log.log_error ~loc:l + "Proj on an inductive type that's not a tuple!"; + etype + | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; etype) + | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = @@ -926,6 +971,7 @@ and fv (e : lexp) : (DB.set * mv_set) = | Sort (_, (StypeOmega | StypeLevel)) -> fv_empty | Builtin _ -> fv_empty | Var (_, i) -> (DB.set_singleton i, mv_set_empty) + | Proj (_, lxp, _) -> fv lxp | Susp (e, s) -> fv (push_susp e s) | Let (_, defs, e) -> let len = List.length defs in @@ -1014,6 +1060,54 @@ and get_type ctx e = | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> DB.sort_omega | Var (((_, _name), _idx) as v) -> lookup_type ctx v + | Proj (l, e, (loc, label)) + -> ( + + let call_split e = + match lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + let etype = lexp_whnf (get_type ctx e) ctx in + let it, aargs = call_split etype in + match lexp'_whnf it ctx, aargs with + | Inductive (_, _, fargs, constructors), aargs + when SMap.cardinal constructors = 1 + -> let rec mksubst s fargs aargs = + match fargs, aargs with + | [], [] -> s + | _farg::fargs, (_ak, aarg)::aargs + -> mksubst (S.cons aarg s) fargs aargs + | _,_ -> (log_tc_error ~loc:l + "Wrong arg number to inductive type!"; s) in + let s = mksubst S.identity fargs aargs in + let (_,fieldtypes) = List.hd (SMap.bindings constructors) in + let rec getfieldtype s (fieldtypes + : (arg_kind * vname * ltype) list) = + match fieldtypes with + | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" + label; + etype + | (ak, (_, Some fn), ftype)::_ when fn = label + (* We found our field! *) + -> if not (ak = Aerasable) + then mkSusp ftype s (* Yay! We found our field! *) + else (log_tc_error ~loc:l + "Can't Proj an erasable field: %s" label; + Lexp.impossible) + | (_, vdef, _)::fieldtypes + -> let fvdef vdef e loc lbl = + match vdef with + |(_, Some _) -> mkProj (loc, e, lbl) + |_ -> Lexp.impossible in + let fieldref = fvdef vdef e l (loc, label) in + getfieldtype (S.cons fieldref s) fieldtypes in + getfieldtype s fieldtypes + | Inductive _, _ + -> Log.log_error ~loc:l + "Proj on an inductive type that's not a tuple!"; + etype + | _,_ -> Log.log_error ~loc:l "Proj on a non-inductive type!" ; + etype) | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in @@ -1140,11 +1234,53 @@ let arity_of_cons ^^ {|because it is not an inductive type: %s|}) name (lexp_string ty) + +let pos_of_label lctx label e : int = + let call_split e = + match lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + + let it, aargs = call_split (lexp_whnf e lctx) in + match lexp'_whnf it lctx, aargs with + | Inductive (_, _, _, constructors), _ + when SMap.cardinal constructors = 1 + -> let (_, st) = label in + (match SMap.bindings constructors with + | [(_,l)] -> let rec find_index + label + (l : (arg_kind * vname * ltype) list) + (c: int) : int = + match l with + | [] + -> let (loc,st) = label in + Log.log_error ~loc:loc "Label Not Found: %s" st; + 0 + | (_, (_, Some vn), _ )::_ when (String.equal vn st) + -> c + | _::tl -> find_index label tl (c + 1) + in + find_index label l 0 + | _ -> let (loc, _) = label in + Log.log_fatal ~loc:loc "Wrong arg number to inductive type!") + | Inductive _, _ + -> let (loc,_) = label in + Log.log_error ~loc:loc "Proj on an inductive type that's not a tuple!"; + 0 + | _,_ -> let (loc,_) = label in + Log.log_error ~loc:loc "Proj on a non-inductive type: %s" + (Lexp.lexp_string it); + 0 + + let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = match lexp_lexp' lxp with | L.Imm (s) -> E.Imm (s) | L.Builtin (v, _) -> E.Builtin (v) | L.Var (v) -> E.Var (v) + | L.Proj (l, exp, label) + -> let t = get_type lctx exp in + E.Proj (l, erase_type lctx exp, pos_of_label lctx label t) | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s) | L.Lambda (P.Aerasable, _, _, body) ===================================== src/positivity.ml ===================================== @@ -1,4 +1,4 @@ -(* Copyright (C) 2021 Free Software Foundation, Inc. +(* Copyright (C) 2021, 2022 Free Software Foundation, Inc. * * Author: Simon Génier <simon.genier(a)umontreal.ca> * Keywords: languages, lisp, dependent types. @@ -116,6 +116,7 @@ and positive' index lexp = * as the Call applies as a degenerate case with no arguments. *) -> true + | Lexp.Proj _ -> false | Lexp.Case _ | Lexp.Cons _ | Lexp.Let _ | Lexp.Sort _ | Lexp.SortLevel _ (* There are no rules that have these synctactic forms as a conclusion. *) ===================================== src/unification.ml ===================================== @@ -1,6 +1,6 @@ (* unification.ml --- Unification of Lexp terms -Copyright (C) 2016-2021 Free Software Foundation, Inc. +Copyright (C) 2016-2022 Free Software Foundation, Inc. Author: Vincent Bonnevalle <tiv.crb(a)gmail.com> @@ -69,6 +69,7 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | Sort (_, (StypeOmega | StypeLevel)) -> false | Builtin _ -> false | Var (_, _i) -> false + | Proj (_,lxp, _) -> oi lxp | Susp (_e, _s) -> Log.internal_error "`e` should be \"clean\" here!?" (* ; oi (push_susp e s) *) | Let (_, defs, e) ===================================== typer.ml ===================================== @@ -40,12 +40,22 @@ let arg_defs = ("-Vfull-lctx", Arg.Set Debruijn.log_full_lctx, - "Print the full lexp context on error."); + "Print the full lexp context on error"); + + ("-Vmacro-expansion", + Arg.Set Elab.macro_tracing_enabled, + "Trace macro expansion"); ] +let parse_args argv usage = + try Arg.parse_argv argv arg_defs add_input_file usage with + | Arg.Help (message) -> + print_string message; + exit 0 + let compile_main argv = let usage = Sys.executable_name ^ " compile [options] <file> …" in - Arg.parse_argv argv arg_defs add_input_file usage; + parse_args argv usage; let ectx = Elab.default_ectx in let backend = new Gambit.gambit_compiler (ectx_to_lctx ectx) stdout in @@ -57,7 +67,7 @@ let compile_main argv = let repl_main argv = let usage = Sys.executable_name ^ " repl [options] [<file>] …" in - Arg.parse_argv argv arg_defs add_input_file usage; + parse_args argv usage; print_string (Fmt.make_title " TYPER REPL "); print_endline " Typer 0.0.0 - Interpreter - (c) 2016-2021"; @@ -80,7 +90,7 @@ let repl_main argv = let run_main argv = let usage = Sys.executable_name ^ " run [options] <file> …" in - Arg.parse_argv argv arg_defs add_input_file usage; + parse_args argv usage; let ectx = Elab.default_ectx in let backend = new Eval.ast_interpreter (ectx_to_lctx ectx) in View it on GitLab: https://gitlab.com/monnier/typer/-/compare/aab4123773bc2a397fcb6a0fc2fe6604… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/aab4123773bc2a397fcb6a0fc2fe6604… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][macro-expansion-tracing] Add a flag to show macros, their arguments and the expanded code.
by Simon Génier (＠ilovemonoids) 16 Fév '22

16 Fév '22

Simon Génier pushed to branch macro-expansion-tracing at Stefan / Typer Commits: aab41237 by Simon Génier at 2022-02-16T19:00:53-05:00 Add a flag to show macros, their arguments and the expanded code. - - - - - 3 changed files: - src/elab.ml - src/log.ml - typer.ml Changes: ===================================== src/elab.ml ===================================== @@ -97,6 +97,12 @@ let lexp_fatal loc lexp = let value_fatal loc value = fatal ~loc ~print_action:(value_print_details value) +let macro_tracing_enabled = ref false +let trace_macro location fmt = + if !macro_tracing_enabled + then Log.log_debug ~loc:location ~section:"MACRO" fmt + else Printf.ifprintf () fmt + (** Type info returned by elaboration. *) type sform_type = | Checked (* Checked that the expression has the requested type. *) @@ -919,21 +925,34 @@ and check_case rtype (loc, target, ppatterns) ctx = mkCase (loc, tlxp, rtype, lpattern, dflt) -and elab_macro_call ctx func args ot = - let t - = match ot with - | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) - (lexp_location func) - | Some t -> t in - let sxp = match lexp_expand_macro (lexp_location func) - func args ctx (Some t) with +and elab_macro_call + (ctx : elab_context) + (func : lexp) + (args : token list) + (ot : ltype option) + : lexp * sform_type = + + let location = lexp_location func in + let t = + match ot with + | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) location + | Some t -> t + in + + trace_macro location {|expanding: %s|} (lexp_string func); + List.iteri + (fun i arg -> arg |> sexp_string |> trace_macro location {|input %d: %s|} i) + args; + let sxp = + match lexp_expand_macro location func args ctx (Some t) with | Vcommand cmd -> (match cmd () with - | Vsexp (sxp) -> sxp - | v -> value_fatal (lexp_location func) v - "Macros should return a IO Sexp") - | v -> value_fatal (lexp_location func) v - "Macros should return an IO" in + | Vsexp (sxp) -> sxp + | v -> value_fatal location v "Macros should return a IO Sexp") + | v -> value_fatal location v "Macros should return an IO" + in + trace_macro location {|output: %s|} (sexp_string sxp); + elaborate ctx sxp ot (* Identify Call Type and return processed call. *) ===================================== src/log.ml ===================================== @@ -114,15 +114,15 @@ let maybe_color_string color_opt str = | None -> str let string_of_log_entry {level; kind; section; loc; msg; _} = - let color = if typer_log_config.color then (level_color level) else None in + let color = if typer_log_config.color then level_color level else None in + let kind_string = Option.value ~default:(string_of_level level) kind in let parens s = "(" ^ s ^ ")" in - (Option.value ~default:"" (Option.map Source.Location.to_string loc) - ^ maybe_color_string - color - (Option.value ~default:(string_of_level level) kind) - ^ ":" - ^ Option.value ~default:"" (Option.map parens section) ^ " " - ^ msg) + sprintf + "%s %s:%s %s" + (Option.value ~default:"" (Option.map Source.Location.to_string loc)) + (maybe_color_string color kind_string) + (Option.value ~default:"" (Option.map parens section)) + msg let print_entry entry = print_endline (string_of_log_entry entry); ===================================== typer.ml ===================================== @@ -40,12 +40,22 @@ let arg_defs = ("-Vfull-lctx", Arg.Set Debruijn.log_full_lctx, - "Print the full lexp context on error."); + "Print the full lexp context on error"); + + ("-Vmacro-expansion", + Arg.Set Elab.macro_tracing_enabled, + "Trace macro expansion"); ] +let parse_args argv usage = + try Arg.parse_argv argv arg_defs add_input_file usage with + | Arg.Help (message) -> + print_string message; + exit 0 + let compile_main argv = let usage = Sys.executable_name ^ " compile [options] <file> …" in - Arg.parse_argv argv arg_defs add_input_file usage; + parse_args argv usage; let ectx = Elab.default_ectx in let backend = new Gambit.gambit_compiler (ectx_to_lctx ectx) stdout in @@ -57,7 +67,7 @@ let compile_main argv = let repl_main argv = let usage = Sys.executable_name ^ " repl [options] [<file>] …" in - Arg.parse_argv argv arg_defs add_input_file usage; + parse_args argv usage; print_string (Fmt.make_title " TYPER REPL "); print_endline " Typer 0.0.0 - Interpreter - (c) 2016-2021"; @@ -80,7 +90,7 @@ let repl_main argv = let run_main argv = let usage = Sys.executable_name ^ " run [options] <file> …" in - Arg.parse_argv argv arg_defs add_input_file usage; + parse_args argv usage; let ectx = Elab.default_ectx in let backend = new Eval.ast_interpreter (ectx_to_lctx ectx) in View it on GitLab: https://gitlab.com/monnier/typer/-/commit/aab4123773bc2a397fcb6a0fc2fe66045… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/aab4123773bc2a397fcb6a0fc2fe66045… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][gambit-compiler-pp] 5 commits: Add a flag to show macros, their arguments and the expanded code.
by Simon Génier (＠ilovemonoids) 16 Fév '22

16 Fév '22

Simon Génier pushed to branch gambit-compiler-pp at Stefan / Typer Commits: 9e0d8f08 by Simon Génier at 2022-02-15T15:42:31-05:00 Add a flag to show macros, their arguments and the expanded code. - - - - - 066cdfab by Simon Génier at 2022-02-15T15:43:24-05:00 Sexp test to ensure the stability of dependent pattern matching. Also improve how discrepancies in sexp tests are reported. - - - - - 2c3200dd by Simon Génier at 2022-02-15T15:43:24-05:00 Pretty-prints the code emitted by the Gambit backend. It spawns Gambit as a subprocess and delegates the pretty-printing to it. We only have to worry about emitting valid code. I intend to use the inferior Gambit mechanism to also implement a REPL. - - - - - a69469e2 by Simon Génier at 2022-02-15T15:43:24-05:00 Adds a simplification phase. It β-reduces let bindings when the value bound is a variable or built-in, i.e. when there is - no-side effect - the value is as fast to evaluate as a variable. The hope is that it will help the readability of the code after macro expantion, without have to rewrite every macro to be smart about expanding to let-expressions. - - - - - edc75e86 by Simon Génier at 2022-02-15T15:43:24-05:00 Introduce an Op record to track operators during parsing. This makes explicit the presence or not of rhs and lhs arguments instead of implicitely tracking them via empty symbols. - - - - - 18 changed files: - src/dune - src/elab.ml - src/fmt.ml - src/gambit.ml - src/lexp.ml - src/log.ml - + src/pretty-printer.scm - src/sexp.ml - + src/simpl.ml - src/subst.ml - tests/dune - tests/gambit_test.ml - tests/lexp_test.ml - + tests/lexp_test_support.ml - tests/sexp_test.ml - + tests/simpl_test.ml - tests/utest_lib.ml - typer.ml Changes: ===================================== src/dune ===================================== @@ -2,4 +2,4 @@ (library (name typerlib) - (libraries zarith str)) + (libraries str unix zarith)) ===================================== src/elab.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2021 Free Software Foundation, Inc. + * Copyright (C) 2011-2022 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -97,6 +97,12 @@ let lexp_fatal loc lexp = let value_fatal loc value = fatal ~loc ~print_action:(value_print_details value) +let macro_tracing_enabled = ref false +let trace_macro location fmt = + if !macro_tracing_enabled + then Log.log_debug ~loc:location ~section:"MACRO" fmt + else Printf.ifprintf () fmt + (** Type info returned by elaboration. *) type sform_type = | Checked (* Checked that the expression has the requested type. *) @@ -919,21 +925,36 @@ and check_case rtype (loc, target, ppatterns) ctx = mkCase (loc, tlxp, rtype, lpattern, dflt) -and elab_macro_call ctx func args ot = - let t - = match ot with - | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) - (lexp_location func) - | Some t -> t in - let sxp = match lexp_expand_macro (lexp_location func) - func args ctx (Some t) with +and elab_macro_call + (ctx : elab_context) + (func : lexp) + (args : token list) + (ot : ltype option) + : lexp * sform_type = + + let location = lexp_location func in + let t = + match ot with + | None + -> + newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) location + | Some t -> t + in + + trace_macro location {|expanding: %s|} (lexp_string func); + List.iteri + (fun i arg -> arg |> sexp_string |> trace_macro location {|input %d: %s|} i) + args; + let sxp = + match lexp_expand_macro location func args ctx (Some t) with | Vcommand cmd -> (match cmd () with - | Vsexp (sxp) -> sxp - | v -> value_fatal (lexp_location func) v - "Macros should return a IO Sexp") - | v -> value_fatal (lexp_location func) v - "Macros should return an IO" in + | Vsexp (sxp) -> sxp + | v -> value_fatal location v "Macros should return a IO Sexp") + | v -> value_fatal location v "Macros should return an IO" + in + trace_macro location {|output: %s|} (sexp_string sxp); + elaborate ctx sxp ot (* Identify Call Type and return processed call. *) @@ -1976,7 +1997,10 @@ let process_file let pretokens = prelex source in let tokens = lex Grammar.default_stt pretokens in let ldecls, ectx' = lexp_p_decls [] tokens ectx in - List.iter backend#process_decls ldecls; + let _, ldecls' = + List.fold_left_map Simpl.simpl_ldecls Subst.identity ldecls + in + List.iter backend#process_decls ldecls'; ectx' with | Sys_error _ ===================================== src/fmt.ml ===================================== @@ -67,12 +67,19 @@ let print_ct_tree i = loop 0 (* Colors *) -let red = "\x1b[31m" -let green = "\x1b[32m" -let yellow = "\x1b[33m" -let magenta = "\x1b[35m" -let cyan = "\x1b[36m" -let reset = "\x1b[0m" +let red_f : _ format6 = "\x1b[31m" +let green_f : _ format6 = "\x1b[32m" +let yellow_f : _ format6 = "\x1b[33m" +let magenta_f : _ format6 = "\x1b[35m" +let cyan_f : _ format6 = "\x1b[36m" +let reset_f : _ format6 = "\x1b[0m" + +let red = string_of_format red_f +let green = string_of_format green_f +let yellow = string_of_format yellow_f +let magenta = string_of_format magenta_f +let cyan = string_of_format cyan_f +let reset = string_of_format reset_f let color_string color str = color ^ str ^ reset ===================================== src/gambit.ml ===================================== @@ -26,6 +26,8 @@ open Elexp type ldecls = Lexp.ldecls type lexp = Lexp.lexp +let gsc_path : string ref = ref "/usr/local/Gambit/bin/gsc" + module Scm = struct type t = | Symbol of string @@ -74,11 +76,11 @@ module Scm = struct let symbol (name : string) : t = Symbol (escape_symbol name) - let rec string_of_exp (exp : t) : string = + let rec to_string (exp : t) : string = match exp with | Symbol (name) -> name | List (elements) - -> "(" ^ String.concat " " (List.map string_of_exp elements) ^ ")" + -> "(" ^ String.concat " " (List.map to_string elements) ^ ")" | String (value) -> let length = String.length value in let buffer = Buffer.create length in @@ -101,7 +103,7 @@ module Scm = struct | Float (value) -> string_of_float value let print (output : out_channel) (exp : t) : unit = - output_string output (string_of_exp exp); + output_string output (to_string exp); output_char output '\n' let describe (exp : t) : string = @@ -282,6 +284,75 @@ let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = | _ -> failwith ("[gambit] unsupported elexp: " ^ elexp_string elexp) +class inferior script_path = + let down_reader, down_writer = Unix.pipe ~cloexec:true () in + let up_reader, up_writer = Unix.pipe ~cloexec:true () in + let _ = Unix.clear_close_on_exec down_reader in + let _ = Unix.clear_close_on_exec up_writer in + let pid = + Unix.create_process + !gsc_path + [|!gsc_path; "-i"; "-f"; script_path|] + down_reader + up_writer + Unix.stderr + in + let _ = Unix.close down_reader in + let _ = Unix.close up_writer in + + object (self) + val pid = pid + val writer_fd = down_writer + val reader_fd = up_reader + val short_buffer = Bytes.make 4 '\x00' + + method stop : unit = + Unix.close writer_fd; + let _ = Unix.waitpid [] pid in + Unix.close reader_fd + + method private read_byte : char = + self#read ~size:1 short_buffer; + Bytes.get short_buffer 0 + + method private write_byte (b : char) : unit = + Bytes.set short_buffer 0 b; + self#write ~size:1 short_buffer + + method private read_sized_string : string = + self#read ~size:4 short_buffer; + let size = Int32.to_int (Bytes.get_int32_be short_buffer 0) in + let buffer = Bytes.create size in + self#read ~size buffer; + Bytes.to_string buffer + + method private write_sized_string (string : string) : unit = + let buffer = Bytes.of_string string in + let size = Bytes.length buffer in + Bytes.set_int32_be short_buffer 0 (Int32.of_int size); + self#write ~size:4 short_buffer; + self#write ~size buffer + + method private read ~(size : int) (bytes : Bytes.t) : unit = + let n = ref 0 in + while !n < size do + n := !n + Unix.read reader_fd bytes !n (size - !n) + done + + method private write ~(size : int) (bytes : Bytes.t) : unit = + assert (Unix.write writer_fd bytes 0 size = size) + end + +class pretty_printer = + object (self) + inherit inferior "src/pretty-printer.scm" + + method pp (expr : Scm.t) : string = + let source = Scm.to_string expr in + self#write_sized_string source; + self#read_sized_string + end + let scheme_of_decl (sctx : ScmContext.t) (name, elexp : string * elexp) : Scm.t = Scm.List ([Scm.define; Scm.Symbol name; scheme_of_expr sctx elexp]) @@ -290,13 +361,19 @@ class gambit_compiler lctx output = object val mutable sctx = ScmContext.of_lctx lctx val mutable lctx = lctx + val pretty_printer = new pretty_printer method process_decls ldecls = let lctx', eldecls = Opslexp.clean_decls lctx ldecls in let sctx', eldecls = List.fold_left_map ScmContext.intro_binding sctx eldecls in - let sdecls = Scm.List (Scm.begin' :: List.map (scheme_of_decl sctx') eldecls) in + let sdecls = List.map (scheme_of_decl sctx') eldecls in sctx <- sctx'; lctx <- lctx'; - Scm.print output sdecls; + List.iter + (fun sdecl -> sdecl |> pretty_printer#pp |> output_string output) + sdecls + + method stop = + pretty_printer#stop end ===================================== src/lexp.ml ===================================== @@ -1,6 +1,6 @@ (* lexp.ml --- Lambda-expressions: the core language. -Copyright (C) 2011-2021 Free Software Foundation, Inc. +Copyright (C) 2011-2022 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> Keywords: languages, lisp, dependent types. @@ -20,6 +20,8 @@ more details. You should have received a copy of the GNU General Public License along with this program. If not, see <http://www.gnu.org/licenses/>. *) +open Printf + module U = Util module L = List module SMap = U.SMap @@ -478,8 +480,6 @@ let rec sunshift n = else (assert (n >= 0); S.cons impossible (sunshift (n - 1))) -let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5))) - (* The quick test below seemed to indicate that about 50% of the "sink"s * are applied on top of another "sink" and hence could be combined into * a single "Lift^n" constructor. Doesn't seem high enough to justify @@ -789,11 +789,10 @@ let rec lexp_unparse lxp = (* FIXME: ¡Unify lexp_print and lexp_string! *) and lexp_string lxp = sexp_string (lexp_unparse lxp) -and subst_string s = match s with - | S.Identity o -> "↑" ^ string_of_int o - | S.Cons (l, s, 0) -> lexp_name l ^ " · " ^ subst_string s - | S.Cons (l, s, o) - -> "(↑"^ string_of_int o ^ " " ^ subst_string (S.cons l s) ^ ")" +and subst_string = function + | S.Identity o -> sprintf "↑%d" o + | S.Cons (l, s, 0) -> sprintf "%s · %s" (lexp_name l) (subst_string s) + | S.Cons (l, s, o) -> sprintf "(↑%d %s)" o (subst_string (S.cons l s)) and lexp_name e = match lexp_lexp' e with ===================================== src/log.ml ===================================== @@ -114,15 +114,15 @@ let maybe_color_string color_opt str = | None -> str let string_of_log_entry {level; kind; section; loc; msg; _} = - let color = if typer_log_config.color then (level_color level) else None in + let color = if typer_log_config.color then level_color level else None in + let kind_string = Option.value ~default:(string_of_level level) kind in let parens s = "(" ^ s ^ ")" in - (Option.value ~default:"" (Option.map Source.Location.to_string loc) - ^ maybe_color_string - color - (Option.value ~default:(string_of_level level) kind) - ^ ":" - ^ Option.value ~default:"" (Option.map parens section) ^ " " - ^ msg) + sprintf + "%s %s:%s %s" + (Option.value ~default:"" (Option.map Source.Location.to_string loc)) + (maybe_color_string color kind_string) + (Option.value ~default:"" (Option.map parens section)) + msg let print_entry entry = print_endline (string_of_log_entry entry); ===================================== src/pretty-printer.scm ===================================== @@ -0,0 +1,44 @@ +(define (read-u8* k) + (let ((b (read-u8))) + (if (eof-object? b) (k)) + b)) + +(define (read-u32be k) + (let ((b3 (read-u8* k)) + (b2 (read-u8* k)) + (b1 (read-u8* k)) + (b0 (read-u8* k))) + (bitwise-ior (arithmetic-shift b3 24) + (arithmetic-shift b2 16) + (arithmetic-shift b1 8) + b0))) + +(define (write-u32be n) + (write-u8 (bitwise-and #xff (arithmetic-shift n -24))) + (write-u8 (bitwise-and #xff (arithmetic-shift n -16))) + (write-u8 (bitwise-and #xff (arithmetic-shift n -8))) + (write-u8 (bitwise-and #xff n))) + +(define (read-sized-string k) + (let* ((bytes-length (read-u32be k)) + (bytes (make-u8vector bytes-length))) + (read-subu8vector bytes 0 bytes-length) + (utf8->string bytes))) + +(define (write-sized-string string) + (let* ((bytes (string->utf8 string)) + (bytes-length (u8vector-length bytes))) + (write-u32be bytes-length) + (write-subu8vector bytes 0 bytes-length) + (force-output (current-output-port)))) + +(call-with-current-continuation + (lambda (k) + (let loop () + (write-sized-string + (with-output-to-string + (lambda () + (with-input-from-string (read-sized-string k) + (lambda () + (pretty-print (read))))))) + (loop)))) ===================================== src/sexp.ml ===================================== @@ -23,6 +23,7 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) open Util open Prelexer open Grammar +open Printf let sexp_error ?print_action loc fmt = Log.log_error ~section:"SEXP" ?print_action ~loc fmt @@ -121,6 +122,61 @@ let sexp_name s = * as appropriate. *) let empty_args_are_not_args = false +module Op = struct + type t = + { head : symbol + ; parts_rev : string list + ; lhs_p : bool + ; rhs_p : bool + } + + let null : t = + { head = (Source.Location.dummy, "") + ; parts_rev = [] + ; lhs_p = false + ; rhs_p = false + } + + let prefix (head : symbol) : t = + {head; parts_rev = []; lhs_p = false; rhs_p = true} + + let postfix (head : symbol) : t = + {head; parts_rev = []; lhs_p = true; rhs_p = false} + + let infix (head : symbol) : t = + {head; parts_rev = []; lhs_p = true; rhs_p = true} + + let compose ({head; parts_rev; lhs_p; rhs_p} : t): symbol = + let (location, head_name) = head in + let name = String.concat "_" (head_name :: List.rev parts_rev) in + let name = + match lhs_p, rhs_p with + | false, false -> name + | false, true -> sprintf "%s_" name + | true, false -> sprintf "_%s" name + | true, true -> sprintf "_%s_" name + in + (location, name) + + let mark_rhs (op : t) : t = + match op.head with + | (_, "") -> op + | _ -> {op with rhs_p = true} + + let push_inner (op : t) (part : string) : t = + let last_name = + match op.parts_rev with + | [] -> snd op.head + | last_name :: _ -> last_name + in + if String.equal part last_name + then op + else {op with parts_rev = part :: op.parts_rev} + + let push_closer (op : t) (part : string) : t = + {op with parts_rev = part :: op.parts_rev; rhs_p = false} +end + (* `op' is the operator being parsed. E.g. for let...in... * it would be either ["let"] or ["in";"let"] depending on which * part we've parsed already. @@ -128,95 +184,104 @@ let empty_args_are_not_args = false * `rargs' are the sexps that compose the arg to the right of the latest * infix symbol. They may belong to `op' or to a later infix operator * we haven't seen yet which binds more tightly. *) -let rec sexp_parse (g : grammar) (rest : sexp list) - (level : int) - (op : symbol list) - (largs : sexp list) - (rargs : sexp list) +let rec sexp_parse + (g : grammar) + (rest : sexp list) + (level : int) + (op : Op.t) + (largs : sexp list) + (rargs : sexp list) : (sexp * sexp list) = - let sexp_parse = sexp_parse g in - let compose_symbol (ss : symbol list) = match ss with - | [] -> (Log.internal_error "empty operator!") - | (l,_)::_ -> (l, String.concat "_" (List.map (fun (_,s) -> s) - (List.rev ss))) in + let sexp_parse = sexp_parse g in - let push_largs largs rargs closer = match List.rev rargs with - | [] -> if closer then dummy_epsilon :: largs else largs - | e::es -> (match es with [] -> e | _ -> Node (e, es)) :: largs in + let push_largs largs rargs closer = + match List.rev rargs with + | [] -> if closer then dummy_epsilon :: largs else largs + | e::es -> (match es with [] -> e | _ -> Node (e, es)) :: largs + in let mk_node op largs rargs closer = let args = List.rev (push_largs largs rargs closer) in - match op with - | [] -> (match args with [] -> dummy_epsilon - | [e] -> e - | e::es -> Node (e, es)) - | ss -> let headname = compose_symbol ss in - match (headname, args) with - (* FIXME: While it's uaulyl good to strip away parens, - * this makes assumptions about the grammar (i.e. there's - * a rule « exp ::= '(' exp ')' » ), and this is sometimes - * not desired (e.g. to distinguish "a b ⊢ c d" from - * "(a b) ⊢ (c d)"). *) - | ((_,"(_)"), [arg]) -> arg (* Strip away parens. *) - | _ -> Node (hSymbol (headname), args) in + let headname = Op.compose op in + match (headname, args) with + (* FIXME: While it's usually good to strip away parens, this makes + assumptions about the grammar (i.e. there's a rule + « exp ::= '(' exp ')' »), and this is sometimes not desired (e.g. to + distinguish "a b ⊢ c d" from "(a b) ⊢ (c d)"). *) + | (_, "(_)"), [arg] -> arg + | _ -> Node (hSymbol (headname), args) + in match rest with - | (((Symbol ((l,name) as s)) as e)::rest') -> - (try match SMap.find name g with - | (None, None) -> sexp_parse rest' level op largs (e::rargs) - | (None, Some rl) (* Open paren or prefix. *) - -> let (e, rest) = sexp_parse rest' rl [s] [] [] - in sexp_parse rest level op largs (e::rargs) - | (Some ll, _) when ll < level - (* A symbol that closes the currently parsed element. *) - -> ((if empty_args_are_not_args then - mk_node (match rargs with [] -> op | _ -> ((l,"")::op)) - largs rargs false - else - mk_node ((l,"")::op) largs rargs true), - rest) - | (Some ll, None) when ll > level - (* A closer without matching opener or a postfix symbol - that binds very tightly. Previously, we signaled an - error (assuming the former), but it prevented the use - tightly binding postfix operators. - - For example, it signaled spurious errors when parsing - expressions with a tightly binding postfix # operator - that implemented record construction by taking an - inductive as argument and returning the inductive's only - constructor. *) - -> sexp_parse rest' level op largs - [mk_node [(l,name);(l,"")] [] rargs true] - | (Some ll, Some rl) when ll > level - (* A new infix which binds more tightly, i.e. does not close - * the current `op' but takes its `rargs' instead. *) - -> let (e, rest) - = if empty_args_are_not_args then - sexp_parse rest' rl - (match rargs with [] -> [s] | _ -> [s;(l,"")]) - (push_largs [] rargs false) [] - else - sexp_parse rest' rl [s;(l,"")] - (push_largs [] rargs true) [] - in sexp_parse rest level op largs [e] - | (Some ll, Some rl) - -> sexp_parse rest' rl - (if ll == rl - && match op with (_,name')::_ -> name = name' - | _ -> false - then op else (s::op)) - (push_largs largs rargs true) [] - | (Some _ll, None) - -> (mk_node (s::op) largs rargs true, rest') - with Not_found -> - sexp_parse rest' level op largs (e::rargs)) - | e::rest -> sexp_parse rest level op largs (e::rargs) - | [] -> (mk_node (match rargs with [] -> op - | _ -> ((dummy_location,"")::op)) - largs rargs false, - []) + | Symbol (_, name as s) as e :: rest' -> + + begin match SMap.find name g with + | (None, None) -> + sexp_parse rest' level op largs (e :: rargs) + + | (None, Some rl) -> + (* Open paren or prefix. *) + let e, rest'' = + sexp_parse rest' rl (Op.prefix s) [] [] + in + sexp_parse rest'' level op largs (e :: rargs) + + | (Some ll, _) when ll < level -> + (* A symbol that closes the currently parsed element. *) + let op' = + match rargs with + | [] when empty_args_are_not_args -> op + | _ -> Op.mark_rhs op + in + mk_node op' largs rargs (not empty_args_are_not_args), rest + + | (Some ll, None) when ll > level -> + (* A closer without matching opener or a postfix symbol that binds very + tightly. Previously, we signaled an error (assuming the former), but + it prevented the use tightly binding postfix operators. + + For example, it signaled spurious errors when parsing expressions + with a tightly binding postfix # operator that implemented record + construction by taking an inductive as argument and returning the + inductive's only constructor. *) + let rargs' = [mk_node (Op.postfix s) [] rargs true] in + sexp_parse rest' level op largs rargs' + + | (Some ll, Some rl) when ll > level -> + (* A new infix which binds more tightly, i.e. does not close the current + `op' but takes its `rargs' instead. *) + let op' = + match rargs with + | [] when empty_args_are_not_args -> Op.prefix s + | _ -> Op.infix s + in + let e, rest'' = + sexp_parse rest' rl op' (push_largs [] rargs (not empty_args_are_not_args)) [] + in + sexp_parse rest'' level op largs [e] + + | (Some ll, Some rl) -> + let op' = if ll = rl then op else Op.push_inner op name in + sexp_parse rest' rl op' (push_largs largs rargs true) [] + + | (Some _ll, None) -> + (* Either a lone postfix or the closer of a mixfix operator. *) + mk_node (Op.push_closer op name) largs rargs true, rest' + + | exception Not_found -> + sexp_parse rest' level op largs (e :: rargs) + end + + | e :: rest -> sexp_parse rest level op largs (e :: rargs) + + | [] -> + let op' = + match rargs with + | [] -> op + | _ -> Op.mark_rhs op + in + mk_node op' largs rargs false, [] let sexp_parse_all grm tokens limit : sexp * token list = let level = match limit with @@ -225,18 +290,21 @@ let sexp_parse_all grm tokens limit : sexp * token list = match SMap.find token grm with | (Some ll, Some _) -> ll + 1 | _ -> Log.internal_error {|Can't find level of "%s"|} token - in let (e, rest) = sexp_parse grm tokens level [] [] [] in - let se = match e with - | Node (Symbol (_, ""), [e]) -> e - | Node (Symbol (_, ""), e::es) -> Node (e, es) - | _ -> (Log.internal_error "Didn't find a toplevel") in - match rest with - | [] -> (se,rest) - | Symbol (l,t) :: rest - -> if not (Some t = limit) - then sexp_error l {|Stray closing token: "%s"|} t; - (se,rest) - | _ -> (Log.internal_error "Stopped parsing before the end!") + in + let e, rest = sexp_parse grm tokens level Op.null [] [] in + let se = + match e with + | Node (Symbol (_, ""), [e]) -> e + | Node (Symbol (_, ""), e::es) -> Node (e, es) + | _ -> Log.internal_error {|Didn't find a toplevel, got: "%s"|} (sexp_string e) + in + match rest with + | [] -> (se,rest) + | Symbol (l,t) :: rest + -> if not (Some t = limit) + then sexp_error l {|Stray closing token: "%s"|} t; + (se,rest) + | _ -> Log.internal_error "Stopped parsing before the end!" (* "sexp_p" is for "parsing" and "sexp_u" is for "unparsing". *) ===================================== src/simpl.ml ===================================== @@ -0,0 +1,164 @@ +(* Copyright (C) 2022 Free Software Foundation, Inc. + * + * Author: Simon Génier <simon.genier(a)umontreal.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. *) + +(** A simplification pass for lexps. It β-reduces let bindings of variables and + builtins. For example, let a = b in a + b + c becomes b + b + c. + + The reason to have such a pass is not so much for performance, but to allow + us to write any macro naively, i.e. we can introduce binding in macros + without fear of “polluting” the generated code. *) + +open Lexp + +(* The secret with the simplification phase is to compute the right + substitution. In the case of a single binding, the correct substitution is + a#1 · ↑1, i.e. replace b#0 with a#1, then shift the rest of the + environment by 1 to account for the sigle remaining binding. + + let a = 1 in let a = 1 in + let b = a[1] in + a[1] + b[0] a[0] + a[0] + + For multiple non-recursive bindings, the situation is similar. In this + example, the substitution is a#2 · b#1 · ↑1, which has the same kind of + substitution for our inlined variable, followed by the identity substitution + of b#1 to b#1, and finally the shift. + + let a = 1 in let a = 1 in + let let + b = 2 b = 2 + c = a[2] + in in + b[1] + c[0] b[0] + a[1] + + What about recursive bindings? We simply don't bother with them! + + *) + +type action = + | Id of vname * int + | SubstVar of vname * int + | SubstConst of lexp + +let compute_subst (min_index : int) (ldecls : ldecls) (subst : subst) : subst = + let loop (name, lexp, _) (actions, i, removed) = + let action, removed = + match lexp with + | Lexp.Var (name, index), _ when index >= min_index + -> SubstVar (name, index), removed + 1 + | Lexp.Builtin _, _ | Lexp.Imm _, _ + -> SubstConst lexp, removed + 1 + | _ + -> Id (name, i), removed + in + action :: actions, i + 1, removed + in + let actions, total, removed = List.fold_right loop ldecls ([], 0, 0) in + let lexps = + let lexp_of_action = function + | Id (name, index) -> Lexp.mkVar (name, index) + | SubstVar (name, index) -> Lexp.mkVar (name, index - removed) + | SubstConst (lexp) -> lexp + in + List.map lexp_of_action actions + in + scompose + (List.fold_left + (fun s e -> Subst.cons e s) + (Subst.shift (total - removed)) + lexps) + subst + +let rec simpl_lexp + (subst : subst) + (lexp : lexp) + : lexp = + + match lexp with + | Lexp.Let (location, ldecls, body), _ + -> let subst', ldecls' = simpl_ldecls subst ldecls in + let body' = simpl_lexp subst' body in + begin match ldecls' with + | [] -> body' + | _ -> Lexp.mkLet (location, ldecls', body') + end + + | Lexp.Lambda (kind, arg_name, arg_ty, body), _ + -> let subst' = ssink arg_name subst in + let body' = simpl_lexp subst' body in + Lexp.mkLambda (kind, arg_name, arg_ty, body') + + | Lexp.Call (head, tail), _ + -> let head' = simpl_lexp subst head in + let tail' = + List.map + (fun (kind, value) -> kind, simpl_lexp subst value) + tail + in + Lexp.mkCall (head', tail') + + | Lexp.Case (location, subject, ty, branches, default), _ + -> let simpl_branch (location, names, body) = + let branch_subst = + ssink + (Source.Location.dummy, None) + (List.fold_left + (fun subst' (_, name) -> ssink name subst') + subst + names) + in + let body' = simpl_lexp branch_subst body in + location, names, body' + in + + let simpl_default (name, body) = + let subst' = ssink name subst in + let body' = simpl_lexp subst' body in + name, body' + in + + let subject' = simpl_lexp subst subject in + let branches' = SMap.map simpl_branch branches in + let default' = Option.map simpl_default default in + Lexp.mkCase (location, subject', ty, branches', default') + + | _ -> mkSusp lexp subst + +and simpl_ldecl + (min_index : int) + (subst : subst) + (ldecls : ldecls) + (name, lexp, ty: ldecl) + : ldecls = + + match lexp with + | Lexp.Var (_, index), _ when index >= min_index -> ldecls + | Lexp.Builtin _, _ | Lexp.Imm _, _ -> ldecls + | _ -> (name, mkSusp lexp subst, ty) :: ldecls + +and simpl_ldecls + (subst : subst) + (ldecls : ldecls) + : subst * ldecls = + + let min_index = List.length ldecls in + let subst' = compute_subst min_index ldecls subst in + let ldecls' = List.fold_left (simpl_ldecl min_index subst') [] ldecls in + subst', List.rev ldecls' ===================================== src/subst.ml ===================================== @@ -1,6 +1,6 @@ (* subst.ml --- Substitutions for Lexp -Copyright (C) 2016-2019 Free Software Foundation, Inc. +Copyright (C) 2016-2022 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> @@ -60,7 +60,7 @@ module U = Util * e[s] % Application of a substitution * * s ::= id % identity substitution - * e . s % replace #0 with `e` and use `s` for the rest + * e · s % replace #0 with `e` and use `s` for the rest * s₁ ∘ s₂ % Composition (apply s₁ *first* and then s₂!). * ↑ % dbi_index = dbi_index + 1 * @@ -72,7 +72,7 @@ module U = Util * e[s] % Application of a substitution * * s ::= id % identity substitution - * e . s % replace #0 by `e` and use `s` for the rest + * e · s % replace #0 by `e` and use `s` for the rest * s ↑n % like Abadi's "s ∘ (↑ⁿ)" * * And the composition ∘ is defined as a function rather than a constructor. @@ -148,7 +148,7 @@ let lookup (mkVar : 'b -> db_index -> 'a) else mkShift e o in lookup' 0 s v -let mkShift s (m:db_offset) = +let mkShift (s : 'a subst) (m : db_offset) : 'a subst = if m>0 then match s with Identity o -> Identity (o + m) | Cons (e, s, o) -> Cons (e, s, o + m) @@ -194,7 +194,7 @@ let compose (mkSusp : 'a -> 'a subst -> 'a) -> (* Myers's fastlane: * if o1 >= sk2 then compose_cons (o1 - sk1) s2' (o + o2') *) if o1 > 0 then compose_cons (o1 - 1) s2 (o + o2) - else + else (* Pull out o2's shift and compose the two Cons. *) let s' = cons e2 s2 in Cons (mkSusp e1 s', compose' s1 s', o + o2) ===================================== tests/dune ===================================== @@ -11,6 +11,7 @@ macro_test positivity_test sexp_test + simpl_test unify_test) (deps (alias %{project_root}/btl/typer_stdlib)) (libraries typerlib) ===================================== tests/gambit_test.ml ===================================== @@ -31,7 +31,7 @@ open Utest_lib open Gambit let fail_on_exp exp = - Printf.printf "in %s\n" (Scm.string_of_exp exp); + Printf.printf "in %s\n" (Scm.to_string exp); false let type_error expected actual = ===================================== tests/lexp_test.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2017 Free Software Foundation, Inc. + * Copyright (C) 2011-2022 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -26,92 +26,36 @@ * --------------------------------------------------------------------------- *) open Typerlib - open Utest_lib +open Lexp_test_support +open Lexp -(* default environment *) let ectx = Elab.default_ectx let rctx = Elab.default_rctx -(* -let _ = (add_test "LEXP" "lexp_print" (fun () -> - - let dcode = " -sqr : (x : Int) -> Int; -sqr = lambda (x : Int) -> - (x * x); - -cube : (x : Int) -> Int; -cube = lambda (x : Int) -> - (x * (sqr x)); - -mult : (x : Int) -> (y : Int) -> Int; -mult = lambda (x : Int) -> - lambda (y : Int) -> - (x * y); - -twice : (y : Int) -> Int; -twice = (mult 2); - -let_fun : (x : Int) -> Int; -let_fun = lambda (x : Int) -> - let a : Int; - a = (twice x); in - let b : Int; - b = (mult 2 x); in - (a + b);" in - - let ret1, _ = lexp_decl_str dcode ectx in - - let to_str decls = - let str = _lexp_str_decls pretty_ppctx (List.flatten ret1) in - List.fold_left (fun str lxp -> str ^ "\n" ^ lxp) "" str in - - (* Cast to string *) - let str1 = (to_str ret1) ^ "\n" in - - print_string str1; - - (* read code again *) - let ret2, _ = lexp_decl_str str1 ectx in - - (* Cast to string *) - let str2 = to_str ret2 in - - if str1 = str2 then success () else failure () -)) *) - -(* -let set_to_list s = - StringSet.fold (fun g a -> g::a) s [] - -let _ = (add_test "LEXP" "Free Variable" (fun () -> - - let dcode = " - a = 2; - b = 3; - f = lambda n -> (a + n); % a is a fv - g = lambda x -> ((f b) + a + x); % f,a,b are fv - " in - - let ret = pexp_decl_str dcode in - let g = match List.rev ret with - | (_, g, _)::_ -> g - | _ -> raise (Unexpected_result "Unexpected empty list") in - - let (bound, free) = free_variable g in - - let bound = set_to_list bound in - let (free, _) = free in - - match bound with - | ["x"] ->( - match free with - | ["_+_"; "f"; "b"; "a"] -> success () - | _ -> failure ()) - | _ -> failure () - -)) *) +let test_lexp name actual expected = + let test () = + let result = expect_equal_lexps [actual] [expected] in + if result = Utest_lib.failure + then Log.print_log () + else Log.clear_log (); + result + in + add_test "LEXP" name test + +let () = + let subst = Subst.cons (make_var 0 "a") Subst.identity in + test_lexp + "Substitute variable" + (Lexp.clean (Lexp.mkSusp (make_var 0 "b") subst)) + (make_var 0 "a") + +let () = + let test () = + if Subst.identity_p (scompose (Subst.shift 5) (sunshift 5)) + then Utest_lib.success + else Utest_lib.failure + in + add_test "LEXP" "unshifts are cancelled by shifts" test -(* run all tests *) let _ = run_all () ===================================== tests/lexp_test_support.ml ===================================== @@ -0,0 +1,45 @@ +(* Copyright (C) 2022 Free Software Foundation, Inc. + * + * Author: Simon Génier <simon.genier(a)umontreal.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. *) + +open Typerlib + +let make_int i = + Lexp.mkImm (Sexp.Integer (Source.Location.dummy, Z.of_int i)) + +let make_sym name = + (Source.Location.dummy, name) + +let make_name name = + (Source.Location.dummy, Some name) + +let make_var index name = + Lexp.mkVar ((Source.Location.dummy, Some name), index) + +let make_builtin name ty = + Lexp.mkBuiltin (name, ty) + +let make_let decls body = + Lexp.mkLet (Source.Location.dummy, decls, body) + +let make_call head args = + Lexp.mkCall (head, List.map (fun arg -> Pexp.Anormal, arg) args) + +let make_1_plus_2 plus_index = + make_call (make_var plus_index "_+_") [make_int 1; make_int 2] ===================================== tests/sexp_test.ml ===================================== @@ -30,16 +30,14 @@ let _ = test_sexp_add "x * x * x" (fun ret -> | _ -> failure ) -let test_sexp_eqv dcode1 dcode2 = - add_test "SEXP" dcode1 - (fun () -> - let s1 = sexp_parse_str dcode1 in - let s2 = sexp_parse_str dcode2 in - if sexp_eq_list s1 s2 - then success - else (sexp_print (List.hd s1); - sexp_print (List.hd s2); - failure)) +let test_sexp_eqv ?name actual_source expected_source = + let test () = + let actual = sexp_parse_str actual_source in + let expected = sexp_parse_str expected_source in + expect_equal_sexps ~actual ~expected + in + let name = Option.value ~default:actual_source name in + add_test "SEXP" name test let _ = test_sexp_eqv "((a) ((1.00)))" "a 1.0" let _ = test_sexp_eqv "(x + y)" "_+_ x y" @@ -51,6 +49,27 @@ let _ = test_sexp_eqv "case e | p1 => e1 | p2 => e2" let _ = test_sexp_eqv "a\\b\\c" "abc" let _ = test_sexp_eqv "(a;b)" "(_\\;_ a b)" let _ = test_sexp_eqv "a.b.c . (.)" "(__\\.__ (__\\.__ a b) c) \\. \\." +let _ = + test_sexp_eqv + ~name:"???" + {| +x = (4 : Int); +y = x; + +p : Eq x y; +p = Eq_refl; + +test : Eq (Eq_cast (p := p) (f := lambda _ -> Unit) ()) (); +test = Eq_refl; + |} + {| +(_=_ x (_:_ 4 Int)); +(_=_ y x); +(_:_ p (Eq x y)); +(_=_ p Eq_refl); +(_:_ test (Eq (Eq_cast (_:=_ p p) (_:=_ f (lambda_->_ _ Unit)) ()) ())); +(_=_ test Eq_refl); + |} (* run all tests *) let _ = run_all () ===================================== tests/simpl_test.ml ===================================== @@ -0,0 +1,103 @@ +(* Copyright (C) 2022 Free Software Foundation, Inc. + * + * Author: Simon Génier <simon.genier(a)umontreal.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. *) + +open Typerlib +open Utest_lib +open Debruijn +open Lexp_test_support + +let test_simpl name original expected = + let test () = + let actual = Simpl.simpl_lexp Subst.identity original in + let result = expect_equal_lexps [actual] [expected] in + if result = Utest_lib.failure + then Log.print_log () + else Log.clear_log (); + result + in + add_test "SIMPL" name test + +let () = + test_simpl + "single let of variable is eliminated" + (make_let [make_name "x", make_var 1 "y", type_int] (make_var 0 "x")) + (make_var 0 "y") + +let () = + test_simpl + "single let of builtin is eliminated" + (make_let + [make_name "x", make_builtin (make_sym "Int") type_int, type0] + (make_var 0 "x")) + (make_builtin (make_sym "Int") type0) + +let () = + test_simpl + "single let of int eliminated" + (make_let + [make_name "x", make_int 3, type_int] + (make_var 0 "x")) + (make_int 3) + +let () = + test_simpl + "first let is eliminated" + (make_let + [make_name "x", make_var 2 "y", type_int; + make_name "z", make_1_plus_2 40, type_int] + (make_var 1 "x")) + (make_let + [make_name "z", make_1_plus_2 39, type_int] + (make_var 1 "y")) + +let () = + test_simpl + "last let is eliminated" + (make_let + [make_name "z", make_1_plus_2 40, type_int; + make_name "x", make_var 2 "y", type_int] + (make_var 0 "x")) + (make_let + [make_name "z", make_1_plus_2 39, type_int] + (make_var 1 "y")) + +let () = + test_simpl + "preserves recursive variables" + (make_let + [make_name "x", make_var 0 "y", type_int; + make_name "y", make_var 1 "x", type_int] + (make_int 5)) + (make_let + [make_name "x", make_var 0 "y", type_int; + make_name "y", make_var 1 "x", type_int] + (make_int 5)) + +let () = + test_simpl + "simplification is transitive" + (make_let + [make_name "x", make_int 55, type_int] + (make_let + [make_name "y", make_var 1 "x", type_int] + (make_var 0 "y"))) + (make_int 55) + +let () = run_all () ===================================== tests/utest_lib.ml ===================================== @@ -132,6 +132,50 @@ let expect_equal_float = _expect_equal_t Float.equal string_of_float let expect_equal_str = _expect_equal_t String.equal (fun g -> g) let expect_equal_values = _expect_equal_t Env.value_eq_list print_value_list +let expect_equal_sexps ~expected ~actual = + let print_sexp_ok s = + Printf.printf (green_f ^^ "%s" ^^ reset_f ^^ "\n") (Sexp.sexp_string s) + in + + let print_sexp_err expected actual = + Printf.printf + ("Expected:\n" ^^ red_f ^^ "%s\n" ^^ reset_f) + (Sexp.sexp_string expected); + Printf.printf + ("Actual:\n" ^^ red_f ^^ "%s\n" ^^ reset_f) + (Sexp.sexp_string actual) + in + + let rec loop failed fine expected actual = + match expected, actual with + | l :: ll, r :: rr -> + if Sexp.sexp_equal l r + then loop failed (l :: fine) ll rr + else + (List.iter print_sexp_ok fine; + print_sexp_err l r; + loop true [] ll rr) + | _ :: _, [] -> + List.iter print_sexp_ok fine; + Printf.printf ("Missing sexps:\n" ^^ red_f); + List.iter (fun s -> s |> Sexp.sexp_string |> Printf.printf "%s\n") expected; + Printf.printf reset_f; + true + | [], _ :: _ -> + List.iter print_sexp_ok fine; + Printf.printf ("Unexpected sexps:\n" ^^ red_f); + List.iter (fun s -> s |> Sexp.sexp_string |> Printf.printf "%s\n") actual; + Printf.printf reset_f; + true + | [], [] -> + if failed + then List.iter print_sexp_ok fine; + failed + in + if loop false [] expected actual + then failure + else success + let expect_equal_lexps = let rec lexp_list_eq l r = match l, r with ===================================== typer.ml ===================================== @@ -40,24 +40,37 @@ let arg_defs = ("-Vfull-lctx", Arg.Set Debruijn.log_full_lctx, - "Print the full lexp context on error."); + "Print the full lexp context on error"); + + ("-Vmacro-expansion", + Arg.Set Elab.macro_tracing_enabled, + "Trace macro expansion"); ] +let parse_args argv usage = + try Arg.parse_argv argv arg_defs add_input_file usage with + | Arg.Help (message) -> + print_string message; + exit 0 + let compile_main argv = let usage = Sys.executable_name ^ " compile [options] <file> …" in - Arg.parse_argv argv arg_defs add_input_file usage; + parse_args argv usage; let ectx = Elab.default_ectx in let backend = new Gambit.gambit_compiler (ectx_to_lctx ectx) stdout in let _ = - List.fold_left (Elab.process_file backend) ectx (list_input_files ()) + Fun.protect + ~finally:(fun () -> backend#stop) + (fun () + -> List.fold_left (Elab.process_file backend) ectx (list_input_files ())) in Log.print_log () let repl_main argv = let usage = Sys.executable_name ^ " repl [options] [<file>] …" in - Arg.parse_argv argv arg_defs add_input_file usage; + parse_args argv usage; print_string (Fmt.make_title " TYPER REPL "); print_endline " Typer 0.0.0 - Interpreter - (c) 2016-2021"; @@ -80,7 +93,7 @@ let repl_main argv = let run_main argv = let usage = Sys.executable_name ^ " run [options] <file> …" in - Arg.parse_argv argv arg_defs add_input_file usage; + parse_args argv usage; let ectx = Elab.default_ectx in let backend = new Eval.ast_interpreter (ectx_to_lctx ectx) in View it on GitLab: https://gitlab.com/monnier/typer/-/compare/f774286c6a0fe70463a8430a6806759b… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/f774286c6a0fe70463a8430a6806759b… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch macro-expansion-tracing
by Simon Génier (＠ilovemonoids) 16 Fév '22

16 Fév '22

Simon Génier pushed new branch macro-expansion-tracing at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/macro-expansion-tracing You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch oops-fix-off-by-one-error-on-line-numbers
by Simon Génier (＠ilovemonoids) 16 Fév '22

16 Fév '22

Simon Génier pushed new branch oops-fix-off-by-one-error-on-line-numbers at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/oops-fix-off-by-one-error-on-line-n… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Février 2022