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

Commits: 94b782ef by Simon Génier at 2019-10-18T21:00:34Z 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,111 @@ +(* 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/. + * + * -------------------------------------------------------------------------- *) + +type db_index = Util.db_index +type lexp = Lexp.lexp + +(** Computes if the judgement x ∉ fv(τ) holds. *) +let rec absent index lexp = + let (fv, _) = Opslexp.fv lexp in + not (Debruijn.set_mem index fv) + +let rec absent_in_bindings index bindings = + match bindings with + | [] -> true + | (_, _, tau) :: bindings -> + absent index tau && absent_in_bindings (index + 1) bindings + +(** Computes if the judgement x ⊢ e pos holds. *) +let rec positive (index : db_index) (lexp : lexp) : bool = + (* + * x ∉ fv(e) + * ─────────── + * x ⊢ e pos + *) + absent index lexp || positive' index lexp + +and positive' index lexp = + match lexp with + | Lexp.Arrow (_, _, tau, _, e) -> + (* + * x ⊢ e pos x ∉ fv(τ) + * ────────────────────── + * x ⊢ (y : τ) → e pos + *) + absent index tau && positive' (index + 1) e + + | Lexp.Call (f, args) -> begin + (* + * x ∉ fv(e⃗) + * ────────────── + * x ⊢ x e⃗ pos + *) + match Lexp.nosusp f with + | Lexp.Var (_, index') when Int.equal index index' -> + List.for_all (fun (_, arg) -> absent index arg) args + | _ -> false + end + + | Lexp.Inductive (_, _, vs, cs) -> + (* + * The rules for μ-types and union types are respectively + * + * x ⊢ e pos x ∉ fv(τ) x ⊢ τ₀ pos x ⊢ τ₁ pos + * ────────────────────── ──────────────────────── + * x ⊢ μy:τ.e pos x ⊢ τ₀ ∪ τ₁ pos + * + * Since the two are not separate in Typer, this rule combines both. + *) + absent_in_bindings index vs + && let index = index + List.length vs in + Util.SMap.for_all (fun _ c -> positive_in_constructor index c) cs + + | Lexp.Susp (e, s) -> + positive' index (Lexp.push_susp e s) + + | Lexp.Var _ -> + (* + * Since we know that x ∉ fv(e), this must be our variable. The same rule + * as the Call applies as a degenerate case with no arguments. + *) + true + + | Lexp.Case _ | Lexp.Cons _ | Lexp.Lambda _ | Lexp.Let _ | Lexp.Sort _ + | Lexp.SortLevel _ -> + (* There are no rules that have these synctactic forms as a conclusion. *) + false + + | Lexp.Metavar _ -> + failwith ( + "positivity check must be done after inference, where metavars are " + ^ "instantiated" + ) + + | Lexp.Builtin _ | Lexp.Imm _ -> + failwith "must never happen since we already know that x ∉ fv(e)" + +and positive_in_constructor index vs = + match vs with + | [] -> true + | (_, _, tau) :: vs -> + positive' index tau && 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, 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/94b782eff7a934fad1e9823c28a8aad168db...