Simon Génier pushed to branch simon-genier at Stefan / Typer

Commits: 4c2bffb9 by Simon Génier at 2019-10-16T21:04:50Z 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,38 @@ +(* 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 + +let rec try_fold (f : 'a -> 'b -> 'a option) (i : 'a) (l : 'b list) : 'a option = + match l with + | head :: tail -> begin + match f i head with + | Some x -> try_fold f x tail + | None -> None + end + | [] -> Some i

===================================== 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,128 @@ +(* 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 is_absent index lexp = + match lexp with + | Lexp.Arrow (_, _, lhs, _, rhs) -> + is_absent index lhs && is_absent (index + 1) rhs + | Lexp.Builtin _ -> + true + | Lexp.Call (f, args) -> + is_absent index f + && List.for_all (fun (_, arg) -> is_absent index arg) args + | Lexp.Case (_, e, ty, branches, default) -> + let check_branches _ e = match e with _, bindings, body -> true in + is_absent index e + && is_absent index ty + && Util.SMap.for_all check_branches branches + && Option.unwrap_or + (Option.map (fun (_, e) -> is_absent index e) 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_absent_in_bindings index vs = + match vs with + | [] -> true + | (_, _, tau) :: vs -> + is_absent index tau && is_absent_in_bindings (index + 1) vs + +let rec is_positive index lexp = + match lexp with + | Lexp.Arrow (_, _, tau, _, e) -> + (* + * x ⊢ e pos x ∉ fv(τ) + * ────────────────────── + * x ⊢ (y : τ) → e pos + *) + is_absent index tau && is_positive (index + 1) e + | Lexp.Builtin _ -> + true + | Lexp.Call (_, args) -> + (* x ∉ fv(e⃗) + * ────────────── + * x ⊢ x e⃗ pos + *) + List.for_all (fun (_, arg) -> is_absent index arg) args + | Lexp.Case _ -> + true + | Lexp.Cons _ -> + true + | Lexp.Imm _ -> + true + | Lexp.Inductive (_, _, vs, cs) -> + (* + * The rule for a plain μ-type is usually something like + * + * x ⊢ e pos x ∉ fv(τ) + * ────────────────────── + * x ⊢ μy:τ.e pos + * + * We use a variant of this rule generalized for Typer's inductive types. + * - They may have more that one arguments, so we must check that our + * variable does not occur in any of the τᵢ. + * - They may have multiple associated data constructors, so we must check + * that all eᵢ are positive in our variable. + *) + is_absent_in_bindings index vs + && let index = index + List.length vs in + Util.SMap.for_all (fun _ c -> is_positive_in_constructor index c) cs + | Lexp.Lambda _ -> + (* TODO raise and error because it is not a proper type? *) + true + | Lexp.Let _ -> + true + | Lexp.Metavar _ -> + true + | Lexp.Sort _ -> + true + | Lexp.SortLevel _ -> + true + | Lexp.Susp _ -> + true + | Lexp.Var _ -> + true + +and is_positive_in_constructor index vs = + match vs with + | [] -> true + | (_, _, tau) :: vs -> + is_positive index tau && is_positive_in_constructor (index + 1) vs

===================================== 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,101 @@ +(* 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 + +type lexp = Lexp.lexp +type vname = Util.vname + +exception WrongPolarity of vname + +type polarity = + | Positive + | Negative + +let print_lexp lexp = ut_string 3 ((Lexp.lexp_string lexp) ^ "\n") + +let assert_polarity polarity lexp vname = + match (polarity, is_positive 0 lexp) with + | (Positive, false) | (Negative, true) -> raise (WrongPolarity vname) + | _ -> () + +let lexp_decl_str (source : string) : (vname * lexp) list = + let (decls, _) = Elab.lexp_decl_str source Elab.default_ectx in + assert (List.length decls > 0); + List.map (fun (vname, lexp, _) -> print_lexp lexp; (vname, lexp)) (List.flatten decls) + +(** + * Check that all the values declared in the source have the given polarity. + * + * Only declarations are checked, you may introduce variables with any polarity + * in the bindings of let or lambda expressions. + *) +let rec check_polarity (polarity : polarity) (source : string) : int = + let decls = lexp_decl_str source in + try + List.iter (fun (vname, lexp) -> assert_polarity polarity lexp vname) decls; + success () + with + | WrongPolarity _ -> failure () + +let add_polarity_test polarity name sample = + add_test "POSITIVITY" name (fun () -> check_polarity polarity sample) + +let add_positivity_test = add_polarity_test Positive + +let add_negativity_test = add_polarity_test Negative + +let () = add_positivity_test "a variable is positive in itself" {| + x : Type; + x = x; +|} + +let () = add_positivity_test "a variable is positive in some other variable" {| + y : Type; + y = Int; + x : Type; + x = y; +|} + +let () = add_positivity_test "an arrow is positive in a variable that appears in its right hand side" {| + x : Type; + x = Int -> x; +|} + +let () = add_negativity_test "an arrow is negative in a variable that appears in its left hand side" {| + x : Type; + x = x -> Int; +|} + +let () = add_positivity_test "an application of a variable is positive if it does not occur in its arguments" {| + GoodList : Type -> Type; + GoodList = typecons (GoodList (a : Type)) (good_nil) (good_cons (GoodList a)); +|} + +let () = add_negativity_test "an application of a variable is negative if it occurs in its arguments" {| + EvilList : Type -> Type; + EvilList = typecons (EvilList (a : Type)) (evil_nil) (evil_cons (EvilList (EvilList a))); +|} + +let () = run_all ()

View it on GitLab: https://gitlab.com/monnier/typer/commit/4c2bffb966c03d59e0d3fe710f1db411078b...