Simon Génier pushed to branch simon-genier at Stefan / Typer
Commits: b2247a87 by Simon Génier at 2019-10-11T02:35:02Z [WIP] Judge if an expression is positive in a variable.
- - - - -
7 changed files:
- + src/list.ml - src/log.ml - + src/option.ml - + src/positivity.ml - src/util.ml - + tests/positivity_test.ml - + tests/select.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,70 @@ +(* 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 + +let test_positivity f name var sample = add_test "POSITIVITY" name (fun () -> + let lexp = List.hd (Elab.lexp_expr_str sample Elab.default_ectx) in + match Select.search_scope "x" lexp with + | Some selected_lexp -> if f (is_positive selected_lexp 0) then success () else failure () + | None -> failure ()) + +let id x = x + +let test_positive = test_positivity id + +let test_negative = test_positivity not + +let _ = test_positive "a variable is positive in itself" "x" "let x = 0 in x" + +let _ = + test_positive "a variable is positive in some other variable" "x" "let y = 1; x = 0 in y" + +let _ = + test_positive + "an arrow is positive in a variable that appears on its right hand side" + "x" + "let x = Int in Int -> x" + +let _ = + test_negative + "an arrow is negative in a variable that appear on the type of its right \ + hand side" + "x" + "let x = Int in x -> Int" + +let _ = + test_positive + "an application of a variable is positive if it does not occur in its \ + arguments" + "x" + "let x = lambda y -> y in x 1" + +let _ = + test_negative + "an application of a variable is negative if it occurs in its arguments" + "x" + "let x = lambda y -> y in x x" + +let _ = run_all ()
===================================== tests/select.ml ===================================== @@ -0,0 +1,72 @@ +(* select.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 nameOf var = match var with _, name -> name + +(* Drills down inside a lexp to find the expression in which a given binding is + * introduced, i.e. where it is the binding at index 0. + *) +let rec search_scope (name : string) (lexp : Lexp.lexp) : Lexp.lexp option = + match lexp with + | Lexp.Arrow (_, v, l, _, r) -> + if Some name = nameOf v + then Some r + else Option.or_else (search_scope name l) (fun () -> search_scope name r) + | Lexp.Builtin _ -> + None + | Lexp.Call (f, args) -> + Option.or_else + (search_scope name f) + (fun () -> List.find_map (function (_, arg) -> search_scope name arg) args) + | Lexp.Case (_, head, _, _branches, _default) -> + search_scope name head + | Lexp.Cons _ -> + None + | Lexp.Imm _ -> + None + | Lexp.Inductive _ -> + None + | Lexp.Lambda _ -> + None + | Lexp.Let (_, bindings, body) -> + search_let name bindings body + | Lexp.Metavar _ -> + None + | Lexp.Sort _ -> + None + | Lexp.SortLevel _ -> + None + | Lexp.Susp _ -> + None + | Lexp.Var (_, other_index) -> + None + +and search_let name bindings body = match bindings with + | ((_, name'), _expr, _ty) :: tail -> ( + if Some name = name' + then match tail with + | _ :: _ -> Some (Lexp.Let (Util.dummy_location, tail, body)) + | [] -> Some body + else search_let name tail body + ) + | [] -> search_scope name body
View it on GitLab: https://gitlab.com/monnier/typer/commit/b2247a87d0dfd7407e426dfd481c7aa6ae8a...
Afficher les réponses par date