Stefan pushed to branch main at Stefan / Typer

Commits: 269f8366 by Stefan Monnier at 2023-07-13T23:50:28-04:00 * btl/pervasive.typer (id): Rename from `I`

- - - - - eac70cf3 by Stefan Monnier at 2023-07-14T00:48:31-04:00 Add the η rule, yay!

- - - - - a4bd5195 by Stefan Monnier at 2023-07-14T00:48:41-04:00 Improve calling convention for builtin reductions

- - - - - 3575175d by James Tan at 2023-07-14T00:48:41-04:00 Add implementation of `Eq` based on the `Interval`

- - - - - 459aad06 by Stefan Monnier at 2023-07-14T00:50:51-04:00 Make the value printer take the type as arg

- - - - -

17 changed files:

- btl/builtins.typer - btl/case.typer - btl/pervasive.typer - btl/poly-lits.typer - debug_util.ml - samples/hott.typer - samples/unerase.typer - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/env.ml - src/eval.ml - src/opslexp.ml - src/unification.ml - tests/elab_test.ml - tests/env_test.ml - tests/eval_test.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -45,10 +45,32 @@ unit = datacons Unit unit; %% The empty type, with no constructors: nothing can have this type. Void = typecons Void;

+%% I = typecons I i0 i1; +i0 = datacons I i0; +i1 = datacons I i1; + +I_not : I -> I; +I_not i = case i + | i0 => i1 + | i1 => i0; + %% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l %% Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l -Eq_refl : ((x : ?t) ≡> Eq x x); -Eq_refl = ##Eq.refl; + +Eq_eq : (l : TypeLevel) ≡> (t : Type_ l) + ≡> (f : I ≡> t) + ≡> Eq (f (_ := i0)) (f (_ := i1)); +Eq_eq = ##Eq.eq; + +Eq_uneq : (l : TypeLevel) ≡> (t : Type_ l) + ≡> (x : t) => (y : t) + => (p : Eq x y) ≡> (i : I) ≡> t; +Eq_uneq = Built-in "Eq.uneq"; + +Eq_refl : (l : TypeLevel) ≡> (t : Type_ l) + ≡> (x : t) ≡> Eq x x; +Eq_refl = lambda _ ≡> lambda _ ≡> lambda x + ≡> Eq_eq (f := lambda _ ≡> x);

Eq_cast : (x : ?) ≡> (y : ?) ≡> (p : Eq x y) @@ -62,14 +84,13 @@ Eq_cast = Built-in "Eq.cast"; %% FIXME: I'd like to just say: %% Eq_comm : Eq ?x ?y -> Eq ?y ?x`; Eq_comm : (x : ?t) ≡> (y : ?t) ≡> Eq x y -> Eq y x; -Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x) - %% FIXME: The code is incorrectly accepted even - %% without this `(p := p)` because we just get a - %% metavar which remains uninstantiated and then - %% the definition gets ignored in the runtime - %% environment (see Eval.from_lctx). - (p := p) - Eq_refl; +Eq_comm p = Eq_eq (f := lambda i ≡> Eq_uneq (p := p) (i := I_not i)); + +%% FIXME: The below code is accepted even in the absence of `p := y=z`. +%% If `y=z` is taken to be unnecessary, this implies that we could define +%% Eq_broken_trans : Eq ?x ?y -> Eq ?x ?z; +Eq_trans : (x : ?t) ≡> (y : ?t) ≡> (z : ?t) ≡> Eq x y -> Eq y z -> Eq x z; +Eq_trans x=y = lambda y=z -> Eq_cast (p := y=z) (f := lambda x' -> Eq x x') x=y;

%% General recursion!! %% Whether this breaks consistency or not is a good question.

===================================== btl/case.typer ===================================== @@ -200,7 +200,7 @@ kinds pat = let ctor-name : Sexp -> String; ctor-name pat = Sexp_dispatch pat (lambda s ss -> ctor-name s) - I strerr strerr strerr strerr; + id strerr strerr strerr strerr; in ctor-name pat;

%% @@ -217,7 +217,7 @@ kinds pat = let %% str_of_sym : Sexp -> String; str_of_sym arg = Sexp_dispatch arg - (lambda _ _ -> "< error >") I strerr strerr strerr strerr; + (lambda _ _ -> "< error >") id strerr strerr strerr strerr;

%% %% map function for all pattern's variables

===================================== btl/pervasive.typer ===================================== @@ -1,6 +1,6 @@ %%% pervasive --- Always available definitions

-%% Copyright (C) 2011-2022 Free Software Foundation, Inc. +%% Copyright (C) 2011-2023 Free Software Foundation, Inc. %% %% Author: Pierre Delaunay pierre.delaunay@hec.ca %% Keywords: languages, lisp, dependent types. @@ -187,7 +187,7 @@ List_empty xs = Int_eq (List_length xs) (Integer->Int 0);

%%% Good 'ol combinators

-I x = x; +id x = x;

%% Use explicit erasable annotations since with an annotation like %% K : ?a -> ?b -> ?a;

===================================== btl/poly-lits.typer ===================================== @@ -18,7 +18,7 @@ typer-immediate = | _ => deflt);

IntegerFromInteger : FromInteger Integer; -IntegerFromInteger = mkFromInteger I; +IntegerFromInteger = mkFromInteger id;

IntFromInteger : FromInteger Int; IntFromInteger = mkFromInteger Integer->Int;

===================================== debug_util.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2020 Free Software Foundation, Inc. + * Copyright (C) 2011-2023 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -177,7 +177,7 @@ let main () = let body = (get_rte_variable (dsinfo, Some "main") main rctx) in

(* eval main *) - print_eval_result 1 body + print_eval_result 1 body None

with Not_found -> ()

===================================== samples/hott.typer ===================================== @@ -59,6 +59,71 @@ %% (x₁ : t(i := i₀)) (x₂ : t(i := i₁)) %% | Hrefl (p : Eq t₁ t₂) (Eq (coe p x₁) x₂);

+%% Example usage of functions based on the Interval +%% type to define equalities +constantString : I ≡> Type; +constantString = lambda _ ≡> String; + +reflString : Eq String String; +reflString = Eq_eq (f := constantString); + +hello : String; +hello = Eq_cast (p := reflString) (f := lambda x -> x) "hello"; + +%% This doesn't work as `helloOrWorld`'s first argument is not erasable, +%% hence we can't prove obviously false equalities. +%% helloOrWorld : I -> String; +%% helloOrWorld s = case s +%% | i0 => "hello" +%% | i1 => "world"; +%% +%% hello=world : Eq "hello" "world"; +%% hello=world = Eq_eq helloOrWorld; + +constantString' : I ≡> Type; +constantString' = Eq_uneq (p := reflString); + +hello2 : Eq_uneq (p := reflString) (i := i0); +hello2 = "hello"; + +hello3 : constantString' (_ := i0); +hello3 = "hello"; + +hello4 : constantString' (_ := i1); +hello4 = "hello"; + +helloRefl : Eq "hello" hello; +helloRefl = Eq_refl; + +%% Functional extensionality +Eq_funext : (f : ? -> ?) => (g : ? -> ?) => + ((x : ?) -> Eq (f x) (g x)) -> + Eq f g; +Eq_funext p = Eq_eq (f := lambda i ≡> lambda x -> Eq_uneq (p := p x) (i := i)); + +%% Properties of the equality type +Eq_cong : (x : ?A) => (y : ?A) => + (f : ?A -> ?) -> (p : Eq x y) + -> Eq (f x) (f y); +Eq_cong f p = Eq_eq (f := lambda i ≡> f (Eq_uneq (p := p) (i := i))); + +%% This is necessary to prove Eq_comm_inv +notnot=id : (i : I) -> Eq i (I_not (I_not i)); +notnot=id i = case i return (Eq i (I_not (I_not i))) + | i0 => Eq_refl + | i1 => Eq_refl; + +%% FIXME: This should be provable, need to reduce `(Eq_comm (Eq_comm p))` to `p`. +%% It should be sufficient to add the following reduction: +%% Eq_uneq (Eq_eq f) i = f (_ := i) +%% and apply `notnot=id`. +%% Eq_comm_inv : (x : ?t) => (y : ?t) => (p : Eq x y) -> Eq (Eq_comm (Eq_comm p)) p; +%% Eq_comm_inv p = ?; + +%% FIXME: Similar to above. +%% Eq_cong_Id : (x : ?t) => (y : ?t) => (p : Eq x y) -> Eq (Eq_cong id p) p; +%% Eq_cong_Id p = ?; + %%%% Univalence

%% type Equiv_function (f : ?A -> ?B) (g : ?A -> ?B)

===================================== samples/unerase.typer ===================================== @@ -1,4 +1,4 @@ %Eq_unerase : Eq ?x ?y ≡> Eq ?x ?y; Eq_unerase = - lambda x y (p : Eq x y) ≡> + lambda x y => lambda (p : Eq x y) ≡> Eq_cast (p := p) (f := Eq x) Eq_refl;

===================================== src/REPL.ml ===================================== @@ -1,6 +1,6 @@ (* REPL.ml --- Read Eval Print Loop (REPL)

-Copyright (C) 2016-2021 Free Software Foundation, Inc. +Copyright (C) 2016-2023 Free Software Foundation, Inc.

Author: Pierre Delaunay pierre.delaunay@hec.ca

@@ -141,13 +141,17 @@ let eval_interactive 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; + let ltypes = List.map (fun lexpr -> OL.check (ectx_to_lctx ectx') lexpr) lexprs in

List.iter interactive#process_decls ldecls; Log.print_log ();

let values = List.map interactive#eval_expr lexprs in - List.iter (Eval.print_eval_result i) values; + List.iter2 (fun v t -> + Eval.print_eval_result i + v + (Some (t, (ectx_to_lctx ectx')))) + values ltypes; Log.print_log ();

ectx'

===================================== src/builtin.ml ===================================== @@ -157,7 +157,8 @@ let register_builtin_csts () = add_builtin_cst "String" DB.type_string; add_builtin_cst "Elab_Context" DB.type_elabctx; add_builtin_cst "Eq" DB.type_eq; - add_builtin_cst "Eq.refl" DB.eq_refl + add_builtin_cst "Eq.eq" DB.eq_eq; + add_builtin_cst "I" DB.type_interval

let type_arrow_0 = mkArrow (dsinfo, Anormal, (dsinfo, None), DB.type0, DB.type0)

===================================== src/debruijn.ml ===================================== @@ -141,23 +141,47 @@ let type_eq_type = mkVar (tv, 1), mkSort (dsinfo, Stype (mkVar (lv, 3))))))) let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) -let eq_refl = + +(* FIXME: Is this the best way to do this? Originally, I wanted to + * define this in Typer and then reference it from OCaml code. + *) +(* Defining the following: + * typecons I i0 i1 + *) +let type_interval + = mkInductive (dsinfo, (dloc, "I"), [], + List.fold_left (fun m name -> SMap.add name [] m) + SMap.empty + ["i0"; "i1"]) + +(* FIXME: Is this the best way to do this? Referencing such a definition + * in Typer will be a pain because it would depend on the location + * in the context. + *) +let interval_i0 = mkCons (type_interval, (dloc, "i0")) +let interval_i1 = mkCons (type_interval, (dloc, "i1")) + +let eq_eq = + (* Variables for the type level, type and the function (I -> ?A) *) let lv = (dsinfo, Some "l") in let tv = (dsinfo, Some "t") in - let xv = (dsinfo, Some "x") in - mkBuiltin ((dloc, "Eq.refl"), - mkArrow (dsinfo, Aerasable, lv, - type_level, - mkArrow (dsinfo, Aerasable, tv, - mkSort (dsinfo, Stype (mkVar (lv, 0))), - mkArrow (dsinfo, Aerasable, xv, - mkVar (tv, 0), - mkCall (dsinfo, type_eq, - [Aerasable, mkVar (lv, 2); - Aerasable, mkVar (tv, 1); - Anormal, mkVar (xv, 0); - Anormal, mkVar (xv, 0)]))))) - + let fv = (dsinfo, Some "f") in + mkBuiltin ((dloc, "Eq.eq"), + mkArrow (dsinfo, Aerasable, lv, + type_level, + mkArrow (dsinfo, Aerasable, tv, + mkSort (dsinfo, Stype (mkVar (lv, 0))), + mkArrow (dsinfo, Aerasable, fv, + mkArrow (dsinfo, Aerasable, (dsinfo, None), + type_interval, + mkVar (tv, 1)), + mkCall (dsinfo, type_eq, + [Aerasable, mkVar (lv, 2); + Aerasable, mkVar (tv, 1); + Anormal, mkCall (dsinfo, mkVar (fv, 0), + [Aerasable, interval_i0]); + Anormal, mkCall (dsinfo, mkVar (fv, 0), + [Aerasable, interval_i1])])))))

(* easier to debug with type annotations *) type env_elem = (vname * varbind * ltype)

===================================== src/env.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018, 2020 Free Software Foundation, Inc. + * Copyright (C) 2011-2023 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -31,12 +31,14 @@ * --------------------------------------------------------------------------- *)

open Elexp +open Lexp open Fmt (* make_title, table util *) open Printf open Sexp

module M = Myers module DB = Debruijn +module OL = Opslexp

let fatal ?print_action ?loc fmt = Log.log_fatal ~section:"ENV" ?print_action ?loc fmt @@ -163,7 +165,35 @@ let rec value_string v = (fun str v -> (str^(value_string v)^";")) "" a) in ("["^(String.sub str 0 ((String.length str) - 1))^"]") )

-let value_print (vtp: value_type) = print_string (value_string vtp) +let value_string_with_type v ltype ctx = + (* Handle some special cases, and use the default + value string otherwise. *) + let rec get_string ltype ctx = + match lexp_lexp' (OL.lexp_whnf ltype ctx) with + | Arrow (_, Aerasable, _, _, ret_ltype) + (* Recurse on return type to handle chain of erasable arguments *) + -> let shifted_ret_ltype = push_susp ret_ltype (S.shift (-1)) in + sprintf "(lambda _ ≡> %s)" (get_string shifted_ret_ltype ctx) + | Call (_, e, args) -> + let e' = OL.lexp_whnf e ctx in + (match args with + (* Pretty print identity types *) + | [_l; (_, t); (_, left); (_, right)] when OL.conv_p ctx e' DB.type_eq + -> sprintf "%s = %s [ %s ]" + (Lexp.to_string left) + (Lexp.to_string right) + (Lexp.to_string t) + | _ -> value_string v) + | _ -> value_string v + in get_string ltype ctx + +(* Caller may optionally provide additional type information + to allow the printer to produce a more informative output. *) +let value_print (vtp: value_type) (lexp_ctx: (lexp * DB.lexp_context) option) = + print_string (Option.fold + ~none:(value_string vtp) + ~some:(fun (ltype, ctx) -> value_string_with_type vtp ltype ctx) + lexp_ctx)

let make_runtime_ctx = M.nil

@@ -192,7 +222,7 @@ let print_rte_ctx_n (ctx: runtime_env) start = | (_, Some m) -> Printf.printf "%-12s | " m | _ -> print_string (make_line ' ' 12); print_string " | " in

- value_print g; print_string "\n") start + value_print g None; print_string "\n") start

(* Only print user defined variables *) let print_rte_ctx ctx =

===================================== src/eval.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018, 2020, 2021, 2022 Free Software Foundation, Inc. + * Copyright (C) 2011-2023 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -404,7 +404,7 @@ let file_read loc _depth args_val = match args_val with * or actually pay attention to the second arg. *) | [Vin channel; Vint _n] -> Vstring (input_line channel) | _ -> error loc ~print_action:(fun _ -> - List.iter (fun v -> value_print v; print_newline ()) args_val; + List.iter (fun v -> value_print v None; print_newline ()) args_val; ) "File.read expects an in_channel. Actual arguments:"

@@ -414,7 +414,7 @@ let file_write loc _depth args_val = match args_val with (* FIXME: This should be the unit value! *) Vundefined) | _ -> error loc ~print_action:(fun _ -> - List.iter (fun v -> value_print v; print_newline ()) args_val; + List.iter (fun v -> value_print v None; print_newline ()) args_val; ) "File.write expects an out_channel and a string. Actual arguments:"

@@ -654,9 +654,9 @@ and sexp_dispatch loc depth args = eval_call blk [Vsexp b]

(* -------------------------------------------------------------------------- *) -and print_eval_result i lxp = +and print_eval_result i lxp ltype = Printf.printf " Out[%02d] >> " i; - value_print lxp; + value_print lxp ltype; print_string "\n";

and print_typer_trace' trace = @@ -765,6 +765,11 @@ let y_operator loc _depth args = | _ -> error loc ("Y expects 1 (function) argument")

let arity0_fun loc _ _ = error loc "Called a 0-arity function!?" + +let eq_uneq loc _ vs = match vs with + | [x; _y] -> x + | _ -> error loc "Eq_uneq takes 2 arguments" + let nop_fun loc _ vs = match vs with | [v] -> v | _ -> error loc "Wrong number of argument to nop" @@ -1050,8 +1055,9 @@ let register_builtin_functions () = ("File.open" , file_open, 2); ("File.read" , file_read, 2); ("File.write" , file_write, 2); - ("Eq.refl" , arity0_fun, 0); ("Eq.cast" , nop_fun, 1); + ("Eq.eq" , arity0_fun, 0); + ("Eq.uneq" , eq_uneq, 2); ("Y" , y_operator, 1); ("Ref.make" , ref_make, 1); ("Ref.read" , ref_read, 1); @@ -1083,8 +1089,7 @@ let _ = register_builtin_functions ()

let builtin_constant v loc _depth args_val = match args_val with (* FIXME: Dummy arg because we currently can't define a Builtin - * *constant* (except for cases like Eq.refl where the contant is not - * actually used). *) + * *constant*. *) | [_] -> v | _ -> error loc "Builtin almost-constant takes a unit argument"

===================================== src/opslexp.ml ===================================== @@ -1,6 +1,6 @@ (* opslexp.ml --- Operations on Lexps

-Copyright (C) 2011-2022 Free Software Foundation, Inc. +Copyright (C) 2011-2023 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -63,7 +63,8 @@ module LMap let reducible_builtins = ref (SMap.empty : (DB.lexp_context -> (P.arg_kind * lexp) list (* The builtin's args *) - -> lexp option) SMap.t) + (* The reduction result and the remaining args *) + -> (lexp * (P.arg_kind * lexp) list) option) SMap.t)

let log_tc_error ?print_action ?loc fmt = Log.log_error ~section:"TC" ?print_action ?loc fmt @@ -190,23 +191,18 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = lexp_whnf (mkCall (l, push_susp body (S.substitute (lexp_whnf arg ctx)), args)) ctx - | Call (l, f', xs1) -> mkCall (l, f', List.append xs1 xs) + | Call (l, f', xs1) -> lexp_whnf (mkCall (l, f', List.append xs1 xs)) ctx | Builtin ((_, name), _) -> (match SMap.find_opt name (!reducible_builtins) with - | Some f -> Option.value ~default:e (f ctx args) + | Some f -> Option.value ~default:e + (Option.map + (fun (e, args) -> + lexp_whnf (mkCall (l, e, args)) ctx) + (f ctx xs)) | None -> e) | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> let e' = lexp_whnf e ctx in - let get_refl e = - let etype = get_type ctx e in (* FIXME we should not need get_type here *) - let elevel = match lexp'_whnf (get_type ctx etype) ctx with - | Sort (_, Stype l) -> l - | _ -> Log.internal_error "" in - mkCall (l, DB.eq_refl, - [Pexp.Aerasable, elevel; - Pexp.Aerasable, etype; - Pexp.Aerasable, e]) in let reduce it name aargs = let targs = match lexp'_whnf it ctx with | Inductive (_,_,fargs,_) -> fargs @@ -224,13 +220,13 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = (S.identity, targs) aargs in (* Substitute case Eq variable by the proof (Eq.refl l t e') *) - let subst = S.cons (get_refl e') subst in + let subst = S.cons (mk_eq_witness l e' ctx) subst in lexp_whnf (push_susp branch subst) ctx with | Not_found -> match default with | Some (_v,default) - -> let subst = S.cons (get_refl e') (S.substitute e') in + -> let subst = S.cons (mk_eq_witness l e' ctx) (S.substitute e') in lexp_whnf (push_susp default subst) ctx | _ -> Log.log_error ~section:"WHNF" ~loc:(Sexp.location l) @@ -289,18 +285,29 @@ and lexp'_whnf e (ctx : DB.lexp_context) : lexp' =

and eq_cast_whnf ctx args = match args with - | [_l; _t; _x; _y; (_, p); _f; (_, fx)] + | _l1 :: _l2 :: _t :: _x :: _y :: (_, p) :: _f :: (_, fx) :: rest -> (match lexp'_whnf p ctx with - | Call (_, refl, _) when conv_p ctx refl DB.eq_refl - -> Some (lexp_whnf fx ctx) + | Call (_, eq, _) when conv_p ctx eq DB.eq_eq + -> Some (fx, rest) | _ -> None) | _ -> None

+and eq_uneq_whnf ctx args = + match args with + | _l :: _t :: (_, x) :: (_, y) :: _p :: (_, i) :: rest + -> if conv_p ctx i DB.interval_i0 + then Some (x, rest) + else if conv_p ctx i DB.interval_i1 + then Some (y, rest) + else None + | _ -> None + and register_reducible_builtins () = reducible_builtins := List.fold_right (fun (n, f) m -> SMap.add n f m) [ - ("Eq.cast", eq_cast_whnf) + ("Eq.cast", eq_cast_whnf); + ("Eq.uneq", eq_uneq_whnf) ] !reducible_builtins

(** A very naive implementation of sets of pairs of lexps. *) @@ -518,12 +525,29 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = (* FIXME Should we use conversion on the terms of the substitution instead of syntactic equality? *) subst_eq s1 s2 + | (Lambda (a, l, t, _) as e', e'') | (e'', (Lambda (a, l, t, _) as e')) + (* Eta expansion of functions *) + -> let expansion = mkLambda (a, l, t, + mkCall (dsinfo, push_susp (hc e'') (S.shift 1), + [(a, mkVar ((dsinfo, None), 0))])) in + conv_p' ctx vs (hc e') expansion | (_, _) -> false

and conv_p (ctx : DB.lexp_context) e1 e2 = if e1 == e2 then true else conv_p' ctx set_empty e1 e2

+and mk_eq_witness sinfo e ctx = + let etype = get_type ctx e in (* FIXME we should not need get_type here *) + let elevel = match lexp'_whnf (get_type ctx etype) ctx with + | Sort (_, Stype l) -> l + | _ -> Log.internal_error "" in + let fn = mkLambda (Pexp.Aerasable, (sinfo, None), etype, e) in + mkCall (sinfo, DB.eq_eq, + [Pexp.Aerasable, elevel; + Pexp.Aerasable, etype; + Pexp.Anormal, fn]) + (********* Testing if a lexp is properly typed *********)

and mkSLlub ctx e1 e2 =

===================================== src/unification.ml ===================================== @@ -1,6 +1,6 @@ (* unification.ml --- Unification of Lexp terms

-Copyright (C) 2016-2022 Free Software Foundation, Inc. +Copyright (C) 2016-2023 Free Software Foundation, Inc.

Author: Vincent Bonnevalle tiv.crb@gmail.com

@@ -248,7 +248,14 @@ and unify' (e1: lexp) (e2: lexp) be substituted with further reduction; 2. Calls, because they might become redexes; 3. Case expressions, for the same reason. *) + + (* FIXME: Does the order of these branches matter? If we can place + the Lambda branches above the Var branches, we can avoid + having to explicitly name the Lambda * Var pair for the + η expansion of Lambdas. *) + | (Lambda _, Var _) -> unify_lambda msl e1' e2' ctx vs' | (_, Var _) -> unify_var e2' e1' ctx + | (Var _, Lambda _) -> unify_lambda msl e2' e1' ctx vs' | (Var _, _) -> unify_var e1' e2' ctx | (_, Call _) -> unify_call msl e2' e1' ctx vs' | (Call _, _) -> unify_call msl e1' e2' ctx vs' @@ -298,7 +305,8 @@ and unify_arrow (matching : scope_level option) (arrow: lexp) (lxp: lexp) ctx vs (** Unify a Lambda and a lexp if possible - Lambda , Lambda -> if var_kind = var_kind then UNIFY ltype & lxp else ERROR - - Lambda , _ -> Impossible + - Lambda , e -> UNIFY lambda with η expansion of e + - else -> Impossible *) and unify_lambda (matching : scope_level option) (lambda: lexp) (lxp: lexp) ctx vs = @@ -311,6 +319,12 @@ and unify_lambda (matching : scope_level option) (DB.lexp_ctx_cons ctx v1 Variable ltype1) (OL.set_shift vs) matching) else [(CKimpossible, ctx, lambda, lxp)] + | (Lambda (arg_kind, arg, ltype, _), e) -> + (* η expansion of Lambda *) + let expansion = mkLambda (arg_kind, arg, ltype, + mkCall (dsinfo, push_susp (hc e) (S.shift 1), + [(arg_kind, mkVar ((dsinfo, None), 0))])) in + unify_lambda matching lambda expansion ctx vs | (_, _) -> [(CKimpossible, ctx, lambda, lxp)]

(** Unify a Metavar and a lexp if possible

===================================== tests/elab_test.ml ===================================== @@ -1,6 +1,6 @@ (* elab_test.ml --- * - * Copyright (C) 2016-2017 Free Software Foundation, Inc. + * Copyright (C) 2016-2023 Free Software Foundation, Inc. * * Author: Vincent Bonnevalle tiv.crb@gmail.com * @@ -255,7 +255,20 @@ let _ = add_elab_test_decl "Check and instantiate implicit args when a type is given" {| test : Int -> ?a -> ?a; -test _ = I; +test _ = id; |}

+let _ = add_elab_test_decl + "η expansion for Lambdas" + {| +succ : Int -> Int; +succ i = i + 1; + +p1 : Eq succ (lambda i -> succ i); +p1 = Eq_refl; + +p2 : Eq (lambda i -> succ i) succ; +p2 = Eq_refl; + |} + let _ = run_all ()

===================================== tests/env_test.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2023 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -67,6 +67,26 @@ let _ = (add_test "ENV" "Set Variables" (fun () -> print_rte_ctx rctx); success))

+let _ = (add_test "ENV" "Value Printer" (fun () -> + let open Lexp in + let exps = [((Vint 42), + (mkArrow (dsinfo, Aerasable, (dsinfo, Some "l"), + DB.type_interval, DB.type_int)), + "(lambda _ ≡> 42)"); + ((Vbuiltin "Eq.eq"), + (mkCall (dsinfo, DB.type_eq, + [Aerasable, mkVar ((dsinfo, None), 2); + Aerasable, DB.type_int; + Anormal, mkVar ((dsinfo, Some "x"), 0); + Anormal, mkVar ((dsinfo, Some "y"), 0)])), + "x = y [ ##Int ]")] in + (* This test assumes that success = 0 and failure = -1 *) + List.fold_left + (fun res (v, ltype, expected) + -> Int.min res + (expect_equal_str (value_string_with_type v ltype DB.empty_lctx) + expected)) + 0 exps))

(* run all tests *) let _ = run_all ()

===================================== tests/eval_test.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2020 Free Software Foundation, Inc. + * Copyright (C) 2011-2023 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -31,7 +31,6 @@ open Utest_lib

open Eval (* reset_eval_trace *)

-open Builtin open Env

(* default environment *) @@ -510,7 +509,7 @@ let _ = test_eval_eqv_named implicitly = ?;

Eq_unerase = - lambda x y (p : Eq x y) ≡> + lambda x y => lambda (p : Eq x y) ≡> Eq_cast (p := p) (f := Eq x) Eq_refl; exfalso (f : False) = ##case_ f; Not p = (contra : p) ≡> False;

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/9bdaed9bd6e4c0c74646fd75e28d1a7bc...