Typer Août 2024

typer@iro.umontreal.ca

1 participants
2 discussions

[Git][monnier/typer][main] Change tuple implementation and behavior of the `_<-_` operator.
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

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

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Août 2024