Typer
Discussions par mois
- ----- 2026 -----
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2025 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2024 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2023 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2022 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2021 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2020 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2019 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2018 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2017 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2016 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
Août 2024
- 1 participants
- 2 discussions
[Git][monnier/typer][main] Change tuple implementation and behavior of the `_<-_` operator.
by Stefan (@monnier) 26 Aoû '24
by Stefan (@monnier) 26 Aoû '24
26 Aoû '24
Stefan pushed to branch main at Stefan / Typer
Commits:
9da75535 by Maxim Bernard at 2024-08-09T16:20:11-04:00
Change tuple implementation and behavior of the `_<-_` operator.
This operator is now used to unpack any `datacons`, possibly with nested
patterns. It also supports the tuple notation.
* btl/assign-datacons.typer:
Implementation of the `assign-datacons` macro, which generates a series
of assignments, each corresponding to a specific value in the provided
datacons.
* btl/pervasive.typer:
Set `_<-_` to newly defined `assign-datacons` macro.
Add `List_filter` function (required by `assign-datacons` module).
Remove definitions: `tuple-nth` macro, pair and triplet (which have been
moved to the tuple module) and `BoolMod`.
Move do-lib definitions and certain List functions further in the file,
since they require definitions in tuple-lib.
* btl/tuple.typer:
Redesign and simplify how Typer implements tuples. Tuples are now one of
the nine predefined ADTs, containing up to 10 items. The comma operator
(defined in `pervasive.typer`) now simply calls the approprate
constructor based on the number of arguments.
* btl/case.typer:
* btl/qcase.typer:
Make necessary adaptations required by changes in tuple implementation.
- - - - -
5 changed files:
- + btl/assign-datacons.typer
- btl/case.typer
- btl/pervasive.typer
- btl/qcase.typer
- btl/tuple.typer
Changes:
=====================================
btl/assign-datacons.typer
=====================================
@@ -0,0 +1,210 @@
+get-symbol-name sexp =
+ let error-msg = "<ERROR: not a symbol>"
+ in Sexp_dispatch sexp
+ (lambda _ _ -> error-msg) % node
+ (lambda name -> name) % symbol
+ (lambda _ -> error-msg) % string
+ (lambda _ -> error-msg) % int
+ (lambda _ -> error-msg) % float
+ (lambda _ -> error-msg); % block
+
+get-constructor-name pattern-sexp =
+ let error-msg = "<ERROR: invalid constructor name>"
+ in Sexp_dispatch pattern-sexp
+ % Must be a node...
+ (lambda head _ ->
+ Sexp_dispatch head
+ (lambda _ _ -> error-msg)
+ % ...whose head is a symbol.
+ (lambda name -> name)
+ (lambda _ -> error-msg)
+ (lambda _ -> error-msg)
+ (lambda _ -> error-msg)
+ (lambda _ -> error-msg))
+ (lambda _ -> error-msg)
+ (lambda _ -> error-msg)
+ (lambda _ -> error-msg)
+ (lambda _ -> error-msg)
+ (lambda _ -> error-msg);
+
+get-subpatterns pattern-sexp =
+ Sexp_dispatch pattern-sexp
+ (lambda _ args -> args)
+ (lambda sym-name -> (cons (Sexp_symbol sym-name) nil))
+ (lambda _ -> nil)
+ (lambda _ -> nil)
+ (lambda _ -> nil)
+ (lambda _ -> nil);
+
+% If `pattern-sexp` is of the form `a,b,c,...`, converts in into the appropriate
+% tuple (e.g. `tuple3 a b c`).
+expand-tuple pattern-sexp =
+ if String_eq "_,_" (get-constructor-name pattern-sexp)
+ then tuple-lib.make-tuple-impl (get-subpatterns pattern-sexp)
+ else pattern-sexp;
+
+% E.g. with argument `(a (b x y) z)`, returns `["x", "y", "z"]`
+get-newvars-names : List Sexp -> List String;
+get-newvars-names subpatterns =
+ List_foldl
+ (lambda acc pat ->
+ Sexp_dispatch pat
+ % node
+ (lambda _head tail ->
+ List_concat acc (get-newvars-names tail))
+ % symbol
+ (lambda name -> List_concat acc (cons name nil))
+ % all other cases should not occur
+ (lambda _ -> acc)
+ (lambda _ -> acc)
+ (lambda _ -> acc)
+ (lambda _ -> acc))
+ nil
+ subpatterns;
+
+pattern-has-var pat var-name =
+ case List_find
+ (lambda candidate -> String_eq var-name candidate)
+ (get-newvars-names (get-subpatterns pat))
+ | some _ => true
+ | none => false;
+
+% Generates a `case` matching over `subject`, which is supposed to have a single
+% constructor `cstr-name` with `nb-params` operands, but only accesses the
+% `var-idx`-th operand, under the bound variable `var-sym`. The branch returns
+% `ret-val`.
+make-single-case : Sexp -> String -> Int -> Int -> Sexp -> Sexp -> Sexp;
+make-single-case subject cstr-name nb-params var-idx var-sym ret-val =
+ let mk-pat-params : Int -> List Sexp;
+ mk-pat-params i =
+ let current-sym = if Int_eq i var-idx
+ then var-sym
+ else (Sexp_symbol "_")
+ in if Int_< i nb-params
+ then cons current-sym (mk-pat-params (Int_+ 1 i))
+ else nil;
+ pattern = (Sexp_node (Sexp_symbol cstr-name) (mk-pat-params 0));
+ branch-node = (Sexp_node (Sexp_symbol "_=>_")
+ (cons pattern (cons ret-val nil)))
+ in Sexp_node (Sexp_symbol "##case_")
+ (cons (Sexp_node (Sexp_symbol "_|_")
+ (cons subject (cons branch-node nil)))
+ nil);
+
+% Generates the `case` cascade that accesses and returns the `var-name` value
+% in `subpatterns`, matching over `subject`.
+make-case-for-var : String -> String -> List Sexp -> Sexp -> Sexp -> Sexp;
+make-case-for-var var-name cstr-name subpatterns subject temp-matching-var =
+ let nb-params = List_length subpatterns;
+ in case List_find (lambda pat-idx-pair ->
+ case pat-idx-pair
+ | pair pat _ => pattern-has-var pat var-name)
+ (List_mapi pair subpatterns)
+ | some found-subpattern =>
+ % There is a corresponding subpattern with a variable named `var-name`.
+ (case found-subpattern
+ | pair pat idx =>
+ Sexp_dispatch
+ pat
+ % node case : has subpatterns
+ (lambda sub-cstr-name sub-subpatterns ->
+ let body = make-case-for-var var-name
+ (get-symbol-name sub-cstr-name)
+ sub-subpatterns
+ temp-matching-var
+ temp-matching-var
+ in make-single-case subject
+ cstr-name
+ nb-params
+ idx
+ temp-matching-var
+ body)
+ % symbol case : is the variable we're looking for
+ (lambda _ ->
+ make-single-case subject
+ cstr-name
+ nb-params
+ idx
+ temp-matching-var
+ temp-matching-var)
+ % other cases : error (cannot occur)
+ (lambda _ -> Sexp_error)
+ (lambda _ -> Sexp_error)
+ (lambda _ -> Sexp_error)
+ (lambda _ -> Sexp_error))
+ | none =>
+ % Logically should not occur
+ Sexp_symbol "error none";
+
+assign-datacons = macro
+ (lambda args ->
+ let
+ pattern-sexp = List_nth 0 args Sexp_error; % e.g. `(a (b x y) z)`
+ value-sexp = List_nth 1 args Sexp_error; % e.g. `someFunction 1 2 3`
+
+ pattern-sexp-norm = expand-tuple pattern-sexp;
+
+ cstr-name = get-constructor-name pattern-sexp-norm;
+ subpatterns = get-subpatterns pattern-sexp-norm;
+
+ new-bound-variables = get-newvars-names subpatterns; % `["x", "y", "z"]`
+
+ make-bound-var-asgn-list datacons-var temp-matching-var =
+ List_map
+ (lambda var-name ->
+ make-decl
+ (Sexp_symbol var-name)
+ (make-case-for-var var-name
+ cstr-name
+ subpatterns
+ datacons-var
+ temp-matching-var))
+ % Only consider variables not named `_`
+ (List_filter
+ (lambda var-name -> not (String_eq var-name "_"))
+ new-bound-variables);
+
+ % Final list of assignments, which contains :
+ % - an unnamed variable with the value being filtered over
+ % - every bound variable from the pattern (`x`, `y` and `z` from the above
+ % example), whose value is a cascade of `case`s returning the appropriate
+ % element from `tuple-varname`
+ % e.g.
+ % gensym0 = someFunction 1 2 3;
+ % x = case gensym0
+ % | a gensym1 _ =>
+ % case gensym1
+ % | b gensym1 _ => gensym1;
+ % y = case gensym0
+ % | a gensym1 _ =>
+ % case gensym1
+ % | b _ gensym1 => gensym1;
+ % z = case gensym0
+ % | a _ gensym1 =>
+ % gensym1;
+ make-defs-list = lambda datacons-var temp-matching-var ->
+ cons (make-decl datacons-var value-sexp)
+ (make-bound-var-asgn-list datacons-var temp-matching-var)
+ in do {
+ datacons-var <- gensym ();
+ temp-matching-var <- gensym ();
+ IO_return (Sexp_node (Sexp_symbol "_;_")
+ (make-defs-list datacons-var temp-matching-var));
+ });
+
+% `(a (b x y) z) <- somevalue`
+test1 = cons (quote (a (b x y) z))
+ (cons (quote somevalue) nil);
+
+% `a, (b x _ z), c <- sometuple`
+test2 = cons (quote (a, (b x _ z), c))
+ (cons (quote sometuple) nil);
+
+runtest test =
+ IO_run
+ (do {
+ res <- Macro_expand assign-datacons test;
+ Sexp_debug_print res;
+ IO_return unit
+ })
+ ();
=====================================
btl/case.typer
=====================================
@@ -610,7 +610,7 @@ in do {
%% Take note that "renamed pattern" correspond to all pattern in list "B"
%% and list "C" is the childs of list "B" in the same order.
%%
-part-type = Pair (Triplet Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) (List (Pair Pats Code));
+part-type = Pair (Tuple Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) (List (Pair Pats Code));
%%
%% Takes a list of branches (pair of (patterns, body))
@@ -716,7 +716,7 @@ partition-branches branches = let
rvars <- gen-vars ivars;
rpat <- renamed-pat pat rvars;
vars <- List_foldl (ff rvars) (IO_return nil) pp;
- IO_return (pair (triplet rpat rvars (List_merge pp vars)) tt);
+ IO_return (pair (rpat, rvars, (List_merge pp vars)) tt);
};
in io-list (List_map mf pre-parts);
@@ -730,7 +730,7 @@ in do {
%% reminder
%%
%% part-type = Pair
-%% (Triplet Pat (List Var) (List (Pair Pat (List (Pair Var Var)))))
+%% (Tuple Pat (List Var) (List (Pair Pat (List (Pair Var Var)))))
%% (List (Pair Pats Code));
%%
@@ -763,8 +763,9 @@ merge-dflt parts odflt = let
preppend : Pat -> List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) ->
part-type -> part-type;
preppend pat vars branches part = case part
- | pair p b => (case p | triplet _ lv v =>
- pair (triplet pat lv (List_concat vars v)) (List_concat branches b));
+ | pair p b =>
+ let (_, lv, v) <- p
+ in pair (pat, lv, (List_concat vars v)) (List_concat branches b);
%%
%% Append child branches if we see more than one default branches
@@ -780,21 +781,22 @@ merge-dflt parts odflt = let
append : Pat -> List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) ->
part-type -> part-type;
append pat vars branches part = case part
- | pair p b => (case p | triplet _ lv v =>
- pair (triplet pat lv (List_concat v vars)) (List_concat b branches));
+ | pair p b =>
+ let (_, lv, v) <- p
+ in pair (pat, lv, (List_concat v vars)) (List_concat b branches);
in case parts
| cons part parts => (case part | pair p pp =>
- (case p | triplet pat _ vars =>
- if (dflt? pat) then
- (case odflt
- | some dflt => merge-dflt parts (some (append pat vars pp dflt))
- | none => merge-dflt parts (some part))
- else
- (case odflt
- %% merge previous default to all branches
- | some dflt => cons (preppend pat vars pp dflt) (merge-dflt parts odflt)
- | none => cons part (merge-dflt parts odflt))))
+ let (pat, _, vars) <- p
+ in if (dflt? pat) then
+ (case odflt
+ | some dflt => merge-dflt parts (some (append pat vars pp dflt))
+ | none => merge-dflt parts (some part))
+ else
+ (case odflt
+ %% merge previous default to all branches
+ | some dflt => cons (preppend pat vars pp dflt) (merge-dflt parts odflt)
+ | none => cons part (merge-dflt parts odflt)))
| nil => (case odflt
| some dflt => (cons dflt nil)
| none => nil);
@@ -840,7 +842,7 @@ in List_map (preppend-dflt max-len) branches;
%% reminder
%%
%% part-type = Pair
-%% (Triplet
+%% (Tuple
%% Pat (List Var) (List (Pair Pat (List (Pair Var Var)))))
%% (List (Pair Pats Code));
%%
@@ -952,11 +954,12 @@ compile-case subjects branches = let
%%
translate-part : part-type -> IO Code;
translate-part branch = case branch
- | pair patterns branches => (case patterns
- | triplet pat rvars pats-vars => do {
- sub-cases <- translate-sub-pats rvars pats-vars branches;
- IO_return (quote (_=>_ (uquote pat) (uquote sub-cases)));
- });
+ | pair patterns branches =>
+ let (pat, rvars, pats-vars) <- patterns
+ in do {
+ sub-cases <- translate-sub-pats rvars pats-vars branches;
+ IO_return (quote (_=>_ (uquote pat) (uquote sub-cases)));
+ };
%%
%% Generate code from all partition
=====================================
btl/pervasive.typer
=====================================
@@ -185,6 +185,16 @@ List_fold2 f o xs ys = case xs
List_empty : List ?a -> Bool;
List_empty xs = Int_eq (List_length xs) (Integer->Int 0);
+% Only keeps items whose `f` predicate returns true
+List_filter : (?a -> Bool) -> List ?a -> List ?a;
+List_filter f l =
+ case l
+ | nil => nil
+ | cons x xs =>
+ (case (f x)
+ | true => cons x (List_filter f xs)
+ | false => List_filter f xs);
+
%%% Good 'ol combinators
id x = x;
@@ -410,55 +420,6 @@ type Sexp_wrapper
Sexp_wrap s = Sexp_dispatch s node symbol string integer float block;
-%%%% Tuples
-
-%% Sample tuple: a module holding Bool and its constructors.
-BoolMod = (##datacons
- %% We need the `?` metavars to be lexically outside of the
- %% `typecons` expression, otherwise they end up generalized, so
- %% we end up with a type constructor like
- %%
- %% typecons _ (cons (τ₁ : Type) (t : τ₁)
- %% (τ₂ : Type) (true : τ₂)
- %% (τ₃ : Type) (false : τ₃))
- %%
- %% And it's actually even worse because it tries to generalize
- %% over the level of those `Type`s, so we end up with an invalid
- %% inductive type.
- ((lambda t1 t2 t3
- -> typecons _ (cons (t :: t1) (true :: t2) (false :: t3)))
- ? ? ?)
- cons)
- (_ := Bool) (_ := true) (_ := false);
-
-Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b));
-pair = datacons Pair pair;
-
-%% Triplet (tuple with 3 values)
-type Triplet (a : Type) (b : Type) (c : Type)
- | triplet (x : a) (y : b) (z : c);
-
-%%%% List with tuple
-
-%% Merge two List to a List of Pair
-%% Both List must be of same length
-List_merge : List ?a -> List ?b -> List (Pair ?a ?b);
-List_merge xs ys = case xs
- | cons x xs => ( case ys
- | cons y ys => cons (pair x y) (List_merge xs ys)
- | nil => nil ) % error
- | nil => nil;
-
-%% `Unmerge` a List of Pair
-%% The two functions name said it all
-List_map-fst xs = let
- mf p = case p | pair x _ => x;
-in List_map mf xs;
-
-List_map-snd xs = let
- mf p = case p | pair _ y => y;
-in List_map mf xs;
-
%%%% Logic
%% `False` should be one of the many empty types.
@@ -600,52 +561,83 @@ typeclass Monad;
define-operator "<-" 80 96;
%%
-%% `List` is the type and `list` is the module
+%% Module containing tuple definitions, including the macro used for expanding
+%% the comma (`_,_`) operator.
+%% Used by `case_` and by `_<-_`
%%
-list = load "btl/list.typer";
+tuple-lib = load "btl/tuple.typer";
+
+Pair = tuple-lib.Pair;
+Tuple3 = tuple-lib.Tuple3;
+Tuple4 = tuple-lib.Tuple4;
+Tuple5 = tuple-lib.Tuple5;
+Tuple6 = tuple-lib.Tuple6;
+Tuple7 = tuple-lib.Tuple7;
+Tuple8 = tuple-lib.Tuple8;
+Tuple9 = tuple-lib.Tuple9;
+Tuple10 = tuple-lib.Tuple10;
+
+pair = tuple-lib.pair;
+tuple3 = tuple-lib.tuple3;
+tuple4 = tuple-lib.tuple4;
+tuple5 = tuple-lib.tuple5;
+tuple6 = tuple-lib.tuple6;
+tuple7 = tuple-lib.tuple7;
+tuple8 = tuple-lib.tuple8;
+tuple9 = tuple-lib.tuple9;
+tuple10 = tuple-lib.tuple10;
%%
-%% Macro `do` for easier series of IO operation
+%% Instantiate a tuple from expressions
%%
%% e.g.:
-%% do { IO_return true; };
+%% tup = (x,y,z);
%%
-do-lib = load "btl/do.typer";
-do-impl = do-lib.do-impl;
-do = do-lib.do;
-do* = do-lib.do*;
+_\,_ = tuple-lib.make-tuple;
-%%
-%% Module containing various macros for tuple
-%% Used by `case_`
-%%
-tuple-lib = load "btl/tuple.typer";
+Tuple = tuple-lib.tuple-type;
%%
-%% Get the nth element of a tuple
+%% Functions over lists of tuples
%%
-%% e.g.:
-%% tuple-nth tup 0;
-%%
-tuple-nth = tuple-lib.tuple-nth;
+
+%% Merge two List to a List of Pair
+%% Both List must be of same length
+List_merge : List ?a -> List ?b -> List (Pair ?a ?b);
+List_merge xs ys = case xs
+ | cons x xs => ( case ys
+ | cons y ys => cons (pair x y) (List_merge xs ys)
+ | nil => nil ) % error
+ | nil => nil;
+
+%% `Unmerge` a List of Pair
+%% The two functions name said it all
+List_map-fst xs = let
+ mf p = case p | pair x _ => x;
+in List_map mf xs;
+
+List_map-snd xs = let
+ mf p = case p | pair _ y => y;
+ in List_map mf xs;
%%
-%% Affectation of tuple
-%%
-%% e.g.:
-%% (x,y,z) <- tup;
+%% `List` is the type and `list` is the module
%%
-_<-_ = tuple-lib.assign-tuple;
+list = load "btl/list.typer";
+
%%
-%% Instantiate a tuple from expressions
+%% Macro `do` for easier series of IO operation
%%
%% e.g.:
-%% tup = (x,y,z);
+%% do { IO_return true; };
%%
-_\,_ = tuple-lib.make-tuple;
+do-lib = load "btl/do.typer";
+do-impl = do-lib.do-impl;
+do = do-lib.do;
+do* = do-lib.do*;
-Tuple = tuple-lib.tuple-type;
+_<-_ = let lib = load "btl/assign-datacons.typer" in lib.assign-datacons;
%%
%% Macro `case` for a some more complex pattern matching
=====================================
btl/qcase.typer
=====================================
@@ -59,12 +59,12 @@ qcase_impl = lambda (sexps : List Sexp) ->
%% Triple of the expression to eliminate, the underlying type A
%% and the relation R
%% A and R are optional
- elim_expr_details : Triplet Sexp (Option Sexp) (Option Sexp);
+ elim_expr_details : Tuple Sexp (Option Sexp) (Option Sexp);
elim_expr_details =
let
- kerr = K (triplet Sexp_error none none);
+ kerr = K (Sexp_error, none, none);
extract_from_annotated_e : Sexp -> List Sexp ->
- Triplet Sexp (Option Sexp) (Option Sexp);
+ Tuple Sexp (Option Sexp) (Option Sexp);
extract_from_annotated_e _ xs =
if (Int_eq (List_length xs) 2)
then
@@ -82,10 +82,10 @@ qcase_impl = lambda (sexps : List Sexp) ->
a = List_nth 0 sexps Sexp_error;
r = List_nth 1 sexps Sexp_error;
in
- triplet e (some a) (some r)
+ (e, (some a), (some r))
else
- triplet e (some Sexp_error) (some Sexp_error);
- kerr' = K (triplet e (some Sexp_error) (some Sexp_error));
+ (e, (some Sexp_error), (some Sexp_error));
+ kerr' = K (e, (some Sexp_error), (some Sexp_error));
in
Sexp_dispatch e_type
extract_type % Nodes
@@ -95,9 +95,9 @@ qcase_impl = lambda (sexps : List Sexp) ->
kerr' % Float
kerr' % List of Sexp
else
- triplet Sexp_error none none;
+ (Sexp_error, none, none);
extract_targ_from_node : Sexp -> List Sexp ->
- Triplet Sexp (Option Sexp) (Option Sexp);
+ Tuple Sexp (Option Sexp) (Option Sexp);
extract_targ_from_node x xs =
%% Check if annotation is present
if (is_sym x "_:_")
@@ -107,12 +107,12 @@ qcase_impl = lambda (sexps : List Sexp) ->
else
%% No annotation was given, return the entire
%% expresson as the elimination target
- triplet x none none;
+ (x, none, none);
in
Sexp_dispatch elim_targ_sexp
extract_targ_from_node % Nodes
- (lambda _ -> triplet elim_targ_sexp
- none none) % Symbol
+ (lambda _ -> (elim_targ_sexp,
+ none, none)) % Symbol
kerr % String
kerr % Integer
kerr % Float
@@ -262,18 +262,18 @@ qcase_impl = lambda (sexps : List Sexp) ->
kerr % Float
kerr; % List of Sexp
qelim_args : List Sexp;
- qelim_args = case elim_expr_details
- | triplet e a r =>
- let
- res = (cons elim_fn
- (cons elim_compat
- (cons e nil)));
- res' = (case r
- | none => res
- | some r' =>
- (cons (build_explicit_arg "R" r') res));
- in
- res';
+ qelim_args =
+ let
+ (e, a, r) <- elim_expr_details;
+ res = (cons elim_fn
+ (cons elim_compat
+ (cons e nil)));
+ res' = (case r
+ | none => res
+ | some r' =>
+ (cons (build_explicit_arg "R" r') res));
+ in
+ res';
qelim_sexp = Sexp_node (Sexp_symbol "Quotient_elim")
qelim_args;
in
=====================================
btl/tuple.typer
=====================================
@@ -1,246 +1,81 @@
%%% tuple.typer --- Notation `_,_` for tuples
-%% Here's an example similar to tuple from `load`
-%%
-%% Sample tuple: a module holding Bool and its constructors.
-%%
-%% We need the `?` metavars to be lexically outside of the
-%% `typecons` expression, otherwise they end up generalized, so
-%% we end up with a type constructor like
-%%
-%% typecons _ (cons (τ₁ : Type) (t : τ₁)
-%% (τ₂ : Type) (true : τ₂)
-%% (τ₃ : Type) (false : τ₃))
-%%
-%% And it's actually even worse because it tries to generalize
-%% over the level of those `Type`s, so we end up with an invalid
-%% inductive type.
-%%
-%% BoolMod = (##datacons
-%% ((lambda t1 t2 t3
-%% -> typecons _ (cons (t :: t1) (true :: t2) (false :: t3)))
-%% ? ? ?)
-%% cons)
-%% (_ := Bool) (_ := true) (_ := false);
-%%
-
-%% List_nth = list.nth;
-%% List_map = list.map;
-%% List_mapi = list.mapi;
-%% List_map2 = list.map2;
-%% List_concat = list.concat;
-
-%%
-%% Move IO outside List (from element to List)
-%% (The function's type explain everything)
-%%
-io-list : List (IO ?a) -> IO (List ?a);
-io-list l = let
- ff : IO (List ?a) -> IO ?a -> IO (List ?a);
- ff o v = do {
- o <- o;
- v <- v;
- IO_return (cons v o);
- };
-in do {
- l <- (List_foldl ff (IO_return nil) l);
- IO_return (List_reverse l nil);
-};
-
-%%
-%% Generate a List of pseudo-unique symbol
-%%
-%% Takes a List of Sexp and generate a List of new name of the same length
-%% whatever are the element of the List
-%%
-gen-vars : List Sexp -> IO (List Sexp);
-gen-vars vars = io-list (List_map
- (lambda _ -> gensym ())
- vars);
-
-%%
-%% Reference for tuple's implicit field name
-%%
-%% Takes a list of vars (it could actually only takes a length)
-%% Returns symbol `%n` with n in [0,length) (integer only, obviously)
-%%
-gen-tuple-names : List Sexp -> List Sexp;
-gen-tuple-names vars = List_mapi
- (lambda _ i -> Sexp_symbol (String_concat "%" (Int->String i)))
- vars;
-
-%%
-%% Takes a list
-%% Returns a list of the same length with every element set to "?" symbol
-%%
-gen-deduce : List Sexp -> List Sexp;
-gen-deduce vars = List_map
- (lambda _ -> Sexp_symbol "?")
- vars;
-
-%%%
-%%% Access one tuple's element
-%%%
-
-%%
-%% This is a macro with conceptualy this signature:
-%% tuple-nth : (tup-type : Type) ≡> (elem-type : Type) ≡> tup-type -> Int -> elem-type;
-%%
-%% Returns the n'th element of the tuple
-%%
-tuple-nth = macro (lambda args -> let
-
- nerr = lambda _ -> (Int->Integer (-1));
-
- %% argument `n` of this macro
- n : Integer;
- n = Sexp_dispatch (List_nth 1 args Sexp_error)
- (lambda _ _ -> nerr ())
- nerr nerr
- (lambda n -> n)
- nerr nerr;
-
- %% implicit tuple field name
- elem-sym : Sexp;
- elem-sym = Sexp_symbol (String_concat "%" (Integer->String n));
-
- %% tuple, argument of this macro
- tup : Sexp;
- tup = List_nth 0 args Sexp_error;
-
-in IO_return (Sexp_node (Sexp_symbol "__.__") (cons tup (cons elem-sym nil)))
-);
-
-%%%
-%%% Affectation, unwraping tuple
-%%%
-
-%%
-%% syntax:
-%% (x, y, z) <- p;
-%%
-%% and then `x`, `y`, `z` are defined as tuple's element 0, 1, 2
-%%
-assign-tuple = macro (lambda args -> let
-
- xserr = lambda _ -> (nil : List Sexp);
-
- %% Expect a ","-node
- %% Returns variables
- get-tup-elem : Sexp -> List Sexp;
- get-tup-elem sexp = Sexp_dispatch sexp
- (lambda s ss ->
- if (Sexp_eq s (Sexp_symbol "_,_")) then
- (ss)
- else
- (nil))
- xserr xserr xserr xserr xserr;
-
- %% map every tuple's variable
- %% using `tuple-nth` to assign element to variable
- mf : Sexp -> Sexp -> Int -> Sexp;
- mf t arg i = Sexp_node (Sexp_symbol "_=_")
- (cons arg (cons (Sexp_node (Sexp_symbol "tuple-nth")
- (cons t (cons (Sexp_integer (Int->Integer i)) nil))) nil));
-
-in do {
- IO_return (Sexp_node (Sexp_symbol "_;_") (List_mapi
- (mf (List_nth 1 args Sexp_error))
- (get-tup-elem (List_nth 0 args Sexp_error))));
-});
-
-%%
-%% Wrap the third argument `fun` with a `let` definition for each variables
-%% Names are taken from `rvars` and definition are taken from `ivars`
-%%
-
-wrap-vars : List Sexp -> List Sexp -> Sexp -> Sexp;
-wrap-vars ivars rvars fun = List_fold2 (lambda fun v0 v1 ->
- %%
- %% I prefer `let` definition because a lambda function would need a type
- %% (quote ((lambda (uquote v0) -> (uquote fun)) (uquote v1))))
- %%
- (quote (let (uquote v1) = (uquote v0) in (uquote fun))))
- fun ivars rvars;
-
-%%
-%% Takes a list of values (expressions) as Sexp (like a variable, 1, 1.0, "str", etc)
-%% Returns a tuple containing those values
-%%
-make-tuple-impl : List Sexp -> IO Sexp;
-make-tuple-impl values = let
-
- %% map tuple element declaration
- mf1 : Sexp -> Sexp -> Sexp;
- mf1 name value = Sexp_node (Sexp_symbol "_::_") (cons name (cons value nil));
-
- %% map tuple element value
- mf2 : Sexp -> Sexp -> Sexp;
- mf2 value nth = Sexp_node (Sexp_symbol "_:=_") (cons nth (cons value nil));
-
- ff1 : Sexp -> Sexp -> Sexp -> Sexp;
- ff1 body arg arg-t = Sexp_node (Sexp_symbol "lambda_->_")
- (cons (Sexp_node (Sexp_symbol "_:_") (cons arg (cons arg-t nil)))
- (cons body nil));
-
- ff2 : Sexp -> Sexp -> Sexp;
- ff2 body arg = Sexp_node (Sexp_symbol "lambda_≡>_")
- (cons (Sexp_node (Sexp_symbol "_:_") (cons arg (cons (Sexp_symbol "Type") nil)))
- (cons body nil));
-
-in do {
- args-t <- gen-vars values;
-
- args <- gen-vars values;
-
- names <- IO_return (gen-tuple-names values);
-
- tuple-t <- IO_return (Sexp_node (Sexp_symbol "typecons")
- (cons (Sexp_symbol "Tuple")
- (cons (Sexp_node (Sexp_symbol "cons") (List_map2 mf1 names args-t)) nil)));
-
- tuple <- IO_return (Sexp_node (Sexp_node (Sexp_symbol "datacons")
- (cons tuple-t (cons (Sexp_symbol "cons") nil)))
- (List_map2 mf2 args names));
-
- fun <- IO_return (List_foldl ff2
- (List_fold2 ff1 tuple (List_reverse args nil)
- (List_reverse args-t nil))
- (List_reverse args-t nil));
-
- values <- IO_return (List_reverse values nil);
-
- affect <- IO_return (Sexp_node fun (List_reverse values nil));
-
- IO_return affect;
-};
-
-%%
-%% Macro to instantiate a tuple
-%%
-make-tuple = macro (lambda args -> do {
- r <- make-tuple-impl args;
- r <- IO_return r;
- IO_return r;
-});
-
-%%
-%% Macro returning the type of a tuple
-%%
-%% Takes element's type as argument
-%%
-tuple-type = macro (lambda args -> let
-
- mf : Sexp -> Sexp -> Sexp;
- mf n t = Sexp_node (Sexp_symbol "_::_")
- (cons n (cons t nil));
-
-in do {
- names <- IO_return (gen-tuple-names args);
-
- r <- IO_return (Sexp_node (Sexp_symbol "typecons") (cons
- (Sexp_symbol "Tuple") (cons (Sexp_node (Sexp_symbol "cons")
- (List_map2 mf names args)) nil)));
-
- IO_return r;
-});
+type Pair (a : Type) (b : Type)
+ | pair (fst : a) (snd : b);
+
+type Tuple3 (a : Type) (b : Type) (c : Type)
+ | tuple3 (v1 : a) (v2 : b) (v3 : c);
+
+type Tuple4 (a : Type) (b : Type) (c : Type) (d : Type)
+ | tuple4 (v1 : a) (v2 : b) (v3 : c) (v4 : d);
+
+type Tuple5 (a : Type) (b : Type) (c : Type) (d : Type) (e : Type)
+ | tuple5 (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e);
+
+type Tuple6 (a : Type) (b : Type) (c : Type) (d : Type) (e : Type) (f : Type)
+ | tuple6 (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e) (v6 : f);
+
+type Tuple7
+ (a : Type) (b : Type) (c : Type) (d : Type) (e : Type)
+ (f : Type) (g : Type)
+ | tuple7
+ (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e)
+ (v6 : f) (v7 : g);
+
+type Tuple8
+ (a : Type) (b : Type) (c : Type) (d : Type) (e : Type)
+ (f : Type) (g : Type) (h : Type)
+ | tuple8
+ (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e)
+ (v6 : f) (v7 : g) (v8 : h);
+
+type Tuple9
+ (a : Type) (b : Type) (c : Type) (d : Type) (e : Type)
+ (f : Type) (g : Type) (h : Type) (i : Type)
+ | tuple9
+ (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e)
+ (v6 : f) (v7 : g) (v8 : h) (v9 : i);
+
+type Tuple10
+ (a : Type) (b : Type) (c : Type) (d : Type) (e : Type)
+ (f : Type) (g : Type) (h : Type) (i : Type) (j : Type)
+ | tuple10
+ (v1 : a) (v2 : b) (v3 : c) (v4 : d) (v5 : e)
+ (v6 : f) (v7 : g) (v8 : h) (v9 : i) (v10 : j);
+
+tuple-cstr-names =
+ cons "pair"
+ (cons "tuple3"
+ (cons "tuple4"
+ (cons "tuple5"
+ (cons "tuple6"
+ (cons "tuple7"
+ (cons "tuple8"
+ (cons "tuple9"
+ (cons "tuple10" nil))))))));
+
+tuple-type-names =
+ cons "Pair"
+ (cons "Tuple3"
+ (cons "Tuple4"
+ (cons "Tuple5"
+ (cons "Tuple6"
+ (cons "Tuple7"
+ (cons "Tuple8"
+ (cons "Tuple9"
+ (cons "Tuple10" nil))))))));
+
+make-sexp-from-names : List String -> List Sexp -> Sexp;
+make-sexp-from-names name-list args =
+ let nb-args = List_length args;
+ tuple-name = List_nth (Int_- nb-args 2) name-list ""
+ in if Int_<= nb-args 10
+ then Sexp_node (Sexp_symbol tuple-name) args
+ else Sexp_symbol "<ERROR: limit 10 items per tuple>";
+
+make-tuple-impl = make-sexp-from-names tuple-cstr-names;
+tuple-type-impl = make-sexp-from-names tuple-type-names;
+
+make-tuple = macro (lambda args -> IO_return (make-tuple-impl args));
+
+tuple-type = macro (lambda args -> IO_return (tuple-type-impl args));
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/9da7553594a3908e07aa8234d5adaf790…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/9da7553594a3908e07aa8234d5adaf790…
You're receiving this email because of your account on gitlab.com.
1
0
[Git][monnier/typer][main] Keep track of residues during elaboration, in case unification becomes
by Stefan (@monnier) 26 Aoû '24
by Stefan (@monnier) 26 Aoû '24
26 Aoû '24
Stefan pushed to branch main at Stefan / Typer
Commits:
b07d2ac3 by Maxim Bernard at 2024-07-16T15:33:20-04:00
Keep track of residues during elaboration, in case unification becomes
possible later.
* src/elab.ml:
Check for remaining residues after elaboration of definitions, but before
generalization.
* src/instargs.ml:
Don't unify when searching for matches, simply check and discard
side-effects (unless a match is found).
* src/unification.ml:
Keep track of residues in a global list, add them each time `unify'` is
to return a `CKresidual`.
Change the behavior of `unify` to only return impossible contraints,
since otherwise it causes errors to be raised on residues.
Provide a `check_unifiable` function to perform unification without
side-effects.
* tests/unify_test.ml:
Adapt tests to account for new `unify` behavior.
- - - - -
4 changed files:
- src/elab.ml
- src/instargs.ml
- src/unification.ml
- tests/unify_test.ml
Changes:
=====================================
src/elab.ml
=====================================
@@ -1428,6 +1428,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
+ Unif.check_no_residues (location e);
+ Unif.clean_residues ();
let g = resolve_instances_and_generalize nctx e in
let e' = g wrapLambda e in
let t' = g (fun ne name t _l e
=====================================
src/instargs.ml
=====================================
@@ -106,7 +106,7 @@ let try_match t1 t2 lctx sl =
List.exists (function | (Unif.CKimpossible,_,_,_) -> true
| _ -> false)
constraints in
- match Unif.unify ~matching:sl t1 t2 lctx with
+ match Unif.check_unifiable ~matching:sl t1 t2 lctx with
| [] -> Match
| constraints when has_impossible constraints -> Impossible
| _ -> Possible
=====================================
src/unification.ml
=====================================
@@ -44,6 +44,32 @@ let create_metavar (ctx : lexp_context) (sl : scope_level) (t : ltype)
let dloc = DB.dloc
let dsinfo = DB.dsinfo
+(* For every definition, keep track of all residues during elaboration. There
+ is a chance they can be unified later (when some metavariable becomes
+ instanciated, for example). *)
+let current_residues = ref ([] : (lexp_context * lexp * lexp) list)
+
+let add_residue (ctx : lexp_context) (e1 : lexp) (e2 : lexp) =
+ current_residues := (ctx, e1, e2) :: !current_residues
+
+let check_no_residues (first_def_loc : Source.Location.t) : unit =
+ (* Raises an error for every remaining residue. *)
+ List.iter
+ (fun (_ctx, lxp1, lxp2) ->
+ Log.log_error
+ ~section:"UNIF"
+ ~loc:first_def_loc
+ ("@[<v>Remaining residue. Can't unify:"
+ ^^ "@, @[<hov 2>%a@]"
+ ^^ "@,with:"
+ ^^ "@, @[<hov 2>%a@]@]")
+ Fmt.pp_print_lexp (clean lxp1)
+ Fmt.pp_print_lexp (clean lxp2))
+ !current_residues
+
+let clean_residues () : unit =
+ current_residues := []
+
(* For convenience *)
type constraint_kind =
| CKimpossible (* Unification is simply impossible. *)
@@ -55,14 +81,6 @@ type constraints = (constraint_kind * lexp_context * lexp * lexp) list
type return_type = constraints
-(* The association of a metavariable must change the scope levels of
- the metavariables that are introduced to a wider scope. Here we
- assume that this has already been done. This happens in `occurs_in`
- during unification. *)
-let associate (id: meta_id) (lxp: lexp) : unit =
- (* FIXME: Check that the types are convertible? *)
- metavar_table := U.IMap.add id (MVal lxp) (!metavar_table)
-
let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with
| MVal _ -> Log.internal_error
"Checking occurrence of an instantiated metavar!!"
@@ -75,7 +93,7 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with
| SortLevel (SLlub (e1, e2)) -> oi e1 || oi e2
| Sort (_, Stype e) -> oi e
| Sort (_, (StypeOmega | StypeLevel)) -> false
- | Builtin _ -> false
+ | Builtin (_, t) -> oi t
| Var (_, _i) -> false
| Proj (_,lxp, _) -> oi lxp
| Susp (_e, _s) -> Log.internal_error "`e` should be \"clean\" here!?"
@@ -115,11 +133,14 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with
metavar_table := U.IMap.add id' (MVar (sl, t, cl))
(!metavar_table);
false) in
- let old_mvt = (!metavar_table) in
+ let old_mvt = !metavar_table in
+ let old_residue_list = !current_residues in
if oi e then
(* Undo the side-effects since we're not going to instantiate the
var after all! *)
- (metavar_table := old_mvt; true)
+ (metavar_table := old_mvt;
+ current_residues := old_residue_list;
+ true)
else false
(* When unifying a metavar with itself, if the two metavars don't
@@ -218,7 +239,39 @@ let rec unify ?(matching : scope_level option)
(e1: lexp) (e2: lexp)
(ctx : lexp_context)
: return_type =
- unify' e1 e2 ctx OL.set_empty matching
+ let constraints = unify' e1 e2 ctx OL.set_empty matching in
+ List.filter (fun (kind, _, _, _) -> kind <> CKresidual) constraints
+
+(* The association of a metavariable must change the scope levels of
+ the metavariables that are introduced to a wider scope. Here we
+ assume that this has already been done. This happens in `occurs_in`
+ during unification. *)
+and associate (id: meta_id) (lxp: lexp) : unit =
+ (* FIXME: Check that the types are convertible? *)
+ metavar_table := U.IMap.add id (MVal lxp) (!metavar_table);
+ (* Go through residues, see if, having instanciated this metavar,
+ we can unify any residue. *)
+ let old_residue_list = !current_residues in
+ (* Reason for purging the list: any lexp pair that is still non-unifiable
+ will be re-added to the list by `unify`. *)
+ clean_residues ();
+ let new_constraints = List.concat_map
+ (fun (ctx, lxp1, lxp2) -> unify lxp1 lxp2 ctx)
+ old_residue_list in
+ (* In case we find out some expressions are impossible to unify,
+ raise an error. *)
+ List.iter
+ (fun (_, _, lxp1, lxp2) ->
+ Log.log_error
+ ~section:"UNIF"
+ ~loc:(location lxp1)
+ ("@[<v>Unresolvable constraint. Expression:"
+ ^^ "@, @[<hov 2>%a@]"
+ ^^ "@,cannot be unified with:"
+ ^^ "@, @[<hov 2>%a@]@]")
+ Fmt.pp_print_lexp (clean lxp1)
+ Fmt.pp_print_lexp (clean lxp2))
+ new_constraints
and unify' (e1: lexp) (e2: lexp)
(ctx : lexp_context) (vs : OL.set_plexp)
@@ -279,8 +332,7 @@ and unify' (e1: lexp) (e2: lexp)
| (Cons _, _) -> unify_cons msl e1' e2' ctx vs'
| _ -> (if OL.conv_p ctx e1' e2' then []
- else ((* print_string "Unification failure on default\n"; *)
- [(CKresidual, ctx, e1, e2)]))
+ else (add_residue ctx e1' e2'; [(CKresidual, ctx, e1, e2)]))
(************************* Type specific unify *******************************)
@@ -341,7 +393,7 @@ and unify_metavar (matching : scope_level option)
"`lexp_whnf` returned an instantiated metavar!!"
| MVar (sl, t, _) -> push_susp t s, sl in
if not (matching_instantiation_check matching sl)
- then [(CKresidual, ctx, lxp1, lxp2)] else
+ then (add_residue ctx lxp1 lxp2; [(CKresidual, ctx, lxp1, lxp2)]) else
match Inverse_subst.apply_inv_subst lxp s with
| exception Inverse_subst.Not_invertible
-> log_info
@@ -351,7 +403,7 @@ and unify_metavar (matching : scope_level option)
^^ "@, @[<hov 2>%a@]@]")
Fmt.pp_print_subst s
pp_print_clean_lexp lxp;
- [(CKresidual, ctx, lxp1, lxp2)]
+ (add_residue ctx lxp1 lxp2; [(CKresidual, ctx, lxp1, lxp2)])
| lxp' when occurs_in idx lxp' -> [(CKimpossible, ctx, lxp1, lxp2)]
| lxp'
-> associate idx lxp';
@@ -370,7 +422,7 @@ and unify_metavar (matching : scope_level option)
pp_print_clean_lexp t
pp_print_clean_lexp (OL.get_type ctx lxp)
pp_print_clean_lexp lxp;
- [(CKresidual, ctx, lxp1, lxp2)] in
+ (add_residue ctx lxp1 lxp2; [(CKresidual, ctx, lxp1, lxp2)]) in
(* FIXME Here, we unify lxp1 with lxp2 again, because that
the metavariables occuring in the associated term might
have different substitutions from the corresponding
@@ -462,7 +514,7 @@ and unify_var (var: lexp) (lxp: lexp) ctx
: return_type =
match (lexp_lexp' var, lexp_lexp' lxp) with
| (Var _, Var _) when OL.conv_p ctx var lxp -> []
- | (_, _) -> [(CKresidual, ctx, var, lxp)]
+ | (_, _) -> (add_residue ctx var lxp; [(CKresidual, ctx, var, lxp)])
(** Unify a Call (call) and a lexp (lxp)
- Call , Call -> UNIFY
@@ -480,7 +532,7 @@ 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)])
+ -> (add_residue ctx call lxp; [(CKresidual, ctx, call, lxp)]))
| (call', lxp') ->
let head_left = match call' with
| Call (_, head_left, _) -> head_left
@@ -501,7 +553,7 @@ and unify_call (matching : scope_level option) (call: lexp) (lxp: lexp) ctx vs
inconvertible heads will remain. *)
[(CKimpossible, ctx, head_left, head_right)]
else
- [(CKresidual, ctx, call, lxp)]
+ (add_residue ctx call lxp; [(CKresidual, ctx, call, lxp)])
(** Unify a Case with a lexp
- Case, Case -> try to unify
@@ -697,3 +749,19 @@ and unify_cons (matching : scope_level option) lxp1 lxp2 ctx vs =
| (Cons (it1, (_, l1)), Cons (it2, (_, l2))) when l1 = l2
-> unify' it1 it2 ctx vs matching
| _, _ -> [(CKimpossible, ctx, lxp1, lxp2)]
+
+(* This function attempts to unify `e1` with `e2`, but discards all
+ side-effects, except if no impossible constraints nor any residues have
+ been found.
+ In the latter case, any instanciated metavariables are kept instanciated. *)
+let check_unifiable ?(matching : scope_level option)
+ (e1: lexp) (e2: lexp)
+ (ctx : lexp_context) =
+ let old_residue_list = !current_residues in
+ let old_metavars = !metavar_table in
+ let unify_result = unify' e1 e2 ctx OL.set_empty matching in
+ current_residues := old_residue_list;
+ match unify_result with
+ | [] -> []
+ | _ -> (metavar_table := old_metavars;
+ unify_result)
=====================================
tests/unify_test.ml
=====================================
@@ -55,16 +55,19 @@ let unif_output ?matching (lxp1: lexp) (lxp2: lexp) ctx =
let orig_subst = !metavar_table in
let constraints = unify ?matching lxp1 lxp2 ctx in
match constraints with
- | []
- -> let new_subst = !metavar_table in
- if orig_subst == new_subst
- then (Equivalent, constraints)
- else (Unification, constraints)
- | (CKresidual, _, _, _)::_ -> (Constraint, constraints)
- | (CKimpossible, _, _, _)::_ -> (Nothing, constraints)
+ | [] ->
+ if !current_residues == [] then
+ let new_subst = !metavar_table in
+ if orig_subst == new_subst
+ then (Equivalent, constraints)
+ else (Unification, constraints)
+ else
+ (Constraint, constraints)
+ | _ -> (Nothing, constraints)
let add_unif_test name ?matching ?(ectx=ectx) lxp_a lxp_b expected =
add_test "UNIFICATION" name (fun () ->
+ clean_residues ();
let (r, _) = unif_output ?matching lxp_a lxp_b (DB.ectx_to_lctx ectx) in
if r = expected then
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b07d2ac397b7ca5b8e78917b0887eb01c…
--
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b07d2ac397b7ca5b8e78917b0887eb01c…
You're receiving this email because of your account on gitlab.com.
1
0