[Typer] [Git][monnier/typer][instance-args] 9 commits: * src/elab.ml: Handle sdforms in a common way.

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@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@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/f2c2fcf1eda126cf2ec8df9169904aefe...