[Git][monnier/typer][simon-genier] [WIP] Judge if an expression is positive in a variable.
Simon Génier pushed to branch simon-genier at Stefan / Typer
Commits: 99dc3728 by Simon Génier at 2019-10-16T13:15:33Z [WIP] Judge if an expression is positive in a variable.
- - - - -
6 changed files:
- + src/list.ml - src/log.ml - + src/option.ml - + src/positivity.ml - src/util.ml - + tests/positivity_test.ml
Changes:
===================================== src/list.ml ===================================== @@ -0,0 +1,29 @@ +(* list.ml --- + * + * Copyright (C) 2019 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. + * + * -------------------------------------------------------------------------- *) + +include Stdlib.List + +let rec find_map (f : 'a -> 'b option) (l : 'a list) : 'b option = + match l with + | head :: tail -> Option.or_else (f head) (fun () -> find_map f tail) + | [] -> None
===================================== src/log.ml ===================================== @@ -119,9 +119,10 @@ let maybe_color_string color_opt str = let string_of_log_entry {level; kind; section; loc; msg} = let color = if typer_log_config.color then (level_color level) else None in let parens s = "(" ^ s ^ ")" in - (option_default "" (option_map string_of_location loc) - ^ maybe_color_string color (option_default (string_of_level level) kind) ^ ":" - ^ option_default "" (option_map parens section) ^ " " + let open Option in + (unwrap_or (map string_of_location loc) "" + ^ maybe_color_string color (unwrap_or kind (string_of_level level)) ^ ":" + ^ unwrap_or (map parens section) "" ^ " " ^ msg)
let print_entry entry =
===================================== src/option.ml ===================================== @@ -0,0 +1,47 @@ +(* option.ml --- + * + * Copyright (C) 2019 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. + * + * -------------------------------------------------------------------------- *) + +let map (f : 'a -> 'b) (o : 'a option) : 'b option = + match o with + | Some x -> Some (f x) + | None -> None + +let and_then (o : 'a option) (f : 'a -> 'b option) : 'b option = + match o with + | Some x -> f x + | None -> None + +let or_else (o : 'a option) (f : unit -> 'a option) : 'a option = + match o with + | Some x -> Some x + | None -> f () + +let unwrap_or (o : 'a option) (d : 'a) : 'a = + match o with + | Some x -> x + | None -> d + +let unwrap_or_else (o : 'a option) (f : unit -> 'a) : 'a = + match o with + | Some x -> x + | None -> f ()
===================================== src/positivity.ml ===================================== @@ -0,0 +1,97 @@ +(* positivity.ml --- + * + * Copyright (C) 2019 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. + * + * -------------------------------------------------------------------------- *) + +let rec absent lexp index = + match lexp with + | Lexp.Arrow (_, _, lhs, _, rhs) -> + absent lhs index && absent rhs (index + 1) + | Lexp.Builtin _ -> + true + | Lexp.Call (f, args) -> + absent f index + && List.for_all (function _, arg -> absent arg index) args + | Lexp.Case (_, e, ty, branches, default) -> + let check_branches _ e = match e with _, bindings, body -> true in + absent e index + && absent ty index + && Util.SMap.for_all check_branches branches + && Option.unwrap_or (Option.map (function _, e -> absent e index) default) true + | Lexp.Cons _ -> + true + | Lexp.Imm _ -> + true + | Lexp.Inductive _ -> + true + | Lexp.Lambda _ -> + true + | Lexp.Let _ -> + true + | Lexp.Metavar _ -> + true + | Lexp.Sort _ -> + true + | Lexp.SortLevel _ -> + true + | Lexp.Susp _ -> + true + | Lexp.Var (_, other_index) -> + index <> other_index + +let rec is_positive lexp index = + match lexp with + | Lexp.Arrow (_, _, tau, _, e) -> + (* x ⊢ e pos x ∉ fv(τ) + * ---------------------- + * x ⊢ (y : τ) → e pos + *) + is_positive e (index + 1) && absent tau index + | Lexp.Builtin _ -> + true + | Lexp.Call (_, args) -> + (* x ∉ fv(e⃗) + * -------------- + * x ⊢ x e⃗ pos + *) + List.for_all (function _, arg -> absent arg index) args + | Lexp.Case _ -> + true + | Lexp.Cons _ -> + true + | Lexp.Imm _ -> + true + | Lexp.Inductive _ -> + true + | Lexp.Lambda _ -> + true + | Lexp.Let _ -> + true + | Lexp.Metavar _ -> + true + | Lexp.Sort _ -> + true + | Lexp.SortLevel _ -> + true + | Lexp.Susp _ -> + true + | Lexp.Var _ -> + true
===================================== src/util.ml ===================================== @@ -58,8 +58,6 @@ let string_sub str b e = String.sub str b (e - b) * `String.uppercase_ascii` is not yet available in Debian stable's `ocaml`. *) let string_uppercase s = String.uppercase s
-let opt_map f x = match x with None -> None | Some x -> Some (f x) - let str_split str sep = let str = String.trim str in let n = String.length str in @@ -106,13 +104,3 @@ let padding_left (str: string ) (dim: int ) (char_: char) : string = let diff = (dim - string_width str) in let lpad = max diff 0 in (String.make lpad char_) ^ str - -let option_default (default : 'a) (opt : 'a option) : 'a = - match opt with - | None -> default - | Some x -> x - -let option_map (fn : 'a -> 'b) (opt : 'a option) : 'b option = - match opt with - | None -> None - | Some x -> Some (fn x)
===================================== tests/positivity_test.ml ===================================== @@ -0,0 +1,95 @@ +(* positivity_test.ml --- + * + * Copyright (C) 2019 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any + * later version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for + * more details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. + * + * -------------------------------------------------------------------------- *) + +open Utest_lib +open Positivity + +exception WrongPolarity of Util.vname + +type polarity = + | Positive + | Negative + +let assert_polarity polarity lexp vname = + match (polarity, is_positive lexp 0) with + | (Positive, false) | (Negative, true) -> raise (WrongPolarity vname) + | _ -> () + +let generate_lexps_from_str str = + let decls = (Elab.lexp_decl_str str Elab.default_ectx) in + let unpack_lexps (es, _) = List.map (fun (_, lexp, _) -> lexp) (List.flatten es) in + let lexps = unpack_lexps decls in + assert (List.length lexps > 0); + lexps + +let rec check_polarity (polarity : polarity) (lexp : Lexp.lexp) : unit = + match lexp with + | Lexp.Let (_, bindings, body) -> + let + check_binding_polarity = fun (vname, value, _) -> + assert_polarity polarity value vname; + check_polarity polarity value + in + List.iter check_binding_polarity bindings; + check_polarity polarity body + | _ -> () + +let test_polarity polarity name sample = add_test "POSITIVITY" name (fun () -> + try + let lexps = generate_lexps_from_str sample in + List.iter (check_polarity polarity) lexps; + success () + with + | WrongPolarity _ -> ut_string 2 "wrong polarity"; failure () (* TODO better error message *) +) + +let test_positive = test_polarity Positive + +let test_negative = test_polarity Negative + +let () = test_positive "a variable is positive in itself" "x : Int; x = x" + +let () = + test_positive "a variable is positive in some other variable" "y : Int; y = 1; x : Int; x = y" + +let () = + test_positive + "an arrow is positive in a variable that appears on its right hand side" + "x : Type; x = Int -> x" + +let () = + test_negative + "an arrow is negative in a variable that appear on the type of its right hand side" + "x : Type; x = x -> Int" + +let () = + test_positive + "an application of a variable is positive if it does not occur in its arguments" + "x : Int -> Int; x _ = x 0" + +let () = + test_negative + "an application of a variable is negative if it occurs in its arguments" + "x : Int -> Int; x _ = x (x 0)" + +let () = run_all ()
View it on GitLab: https://gitlab.com/monnier/typer/commit/99dc3728beee59701f588b777200d20f856b...
Afficher les réponses par date
+let rec absent lexp index =
You can use `fv` (in opslexp.ml) to get the set of freevars (this gets cached, so it's cheap) instead of having to traverse the term by hand.
+let rec is_positive lexp index =
- match lexp with
- | Lexp.Arrow (_, _, tau, _, e) ->
(* x ⊢ e pos x ∉ fv(τ)* ----------------------* x ⊢ (y : τ) → e pos*)is_positive e (index + 1) && absent tau index- | Lexp.Builtin _ ->
true- | Lexp.Call (_, args) ->
(* x ∉ fv(e⃗)* --------------* x ⊢ x e⃗ pos*)List.for_all (function _, arg -> absent arg index) args
Notice that the rule you quote talks about the case `Call (f, args)` where `f` is equal to `index`. Here you don't even look at the function that's called. If it's `index`, then everything's good, and if `absent f index`, everything's good as well, but otherwise we're in trouble.
- | Lexp.Case _ ->
true
When in doubt, return `false` rather than `true` (applies to many of the other cases you have). I think we could return `true` here in *some* cases, but definitely not in general.
- | Lexp.Metavar _ ->
true
This one should be either impossible (i.e. signal an error) or should lookup the metavar in the metavar table and recurse on the result: when we check positivity, inference is presumably done, so all metavars should have been instantiated.
- | Lexp.Susp _ ->
true
No, here you need to apply `push_susp` and then recurse on the result.
- | Lexp.Var _ ->
true
I think one is right ;-)
Stefan
-
Simon Génier -
Stefan Monnier