Simon Génier pushed to branch master at Stefan / Typer
Commits: f8c0ef45 by Simon Génier at 2021-04-28T13:53:58-04:00 Consolidate location related code into Source.
The purpose of this changeset is to take all the Location related code and to move it into the Source module. I kept the aliases in Util for now to reduce the size of this changeset, but it was inevitable that I had to add a few `let open Source.Location in` because of how fields work in OCaml (not great). Fortunately, most of these will disappear as I move more and more location related code inside the source object.
I rewrote a few places to use printf instead of a series of prints, which I think are clearer. The only externally visible change is that I merged two functions that printed location in a different way. Some debug code used to print something like "Ln 32, cl 1", but now prints "foo.typer:32:1" like everywhere else.
- - - - - 8ce3d27f by Simon Génier at 2021-05-10T15:14:17-04:00 Add code to check if a type declaration is positive.
- - - - - 4d0dff15 by Simon Génier at 2021-05-12T15:55:42-04:00 Merge branch 'origin/consolidate-location'
- - - - - f2d6d5df by Simon Génier at 2021-05-12T15:56:34-04:00 Merge branch positivity
- - - - -
13 changed files:
- src/debug.ml - src/elab.ml - src/eval.ml - src/log.ml - src/opslexp.ml - + src/positivity.ml - src/prelexer.ml - src/sexp.ml - src/source.ml - src/util.ml - tests/dune - tests/lexer_test.ml - + tests/positivity_test.ml
Changes:
===================================== src/debug.ml ===================================== @@ -40,12 +40,12 @@ open Prelexer open Sexp open Lexp
+let print_info (message : string) (location : Source.Location.t) : unit = + Printf.printf "%s[%s]" message (Source.Location.to_string location) + (* Print aPretokens *) let debug_pretokens_print pretoken = print_string " "; - let print_info msg loc = - print_string msg; - print_string "["; loc_print loc; print_string "]\t" in
match pretoken with | Preblock(loc, pts,_) @@ -66,9 +66,6 @@ let debug_pretokens_print_all pretokens =
(* Sexp Print *) let debug_sexp_print sexp = - let print_info msg loc = - print_string msg; - print_string "["; loc_print loc; print_string "]\t" in match sexp with | Symbol(_, "") -> print_string "Epsilon " (* "ε" *) @@ -111,9 +108,7 @@ let debug_pexp_print ptop = print_string " "; let l = sexp_location ptop in let print_info msg loc pex = - print_string msg; print_string "["; - loc_print loc; - print_string "]\t"; + print_info msg loc; sexp_print pex in print_info (sexp_name ptop) l ptop
@@ -124,7 +119,7 @@ let debug_lexp_decls decls =
print_string " "; lalign_print_string (lexp_name lxp) 15; - print_string "["; loc_print loc; print_string "]"; + Printf.printf "[%s]" (Source.Location.to_string loc);
let str = lexp_str_decls (!debug_ppctx) [e] in
===================================== src/elab.ml ===================================== @@ -1288,12 +1288,15 @@ and lexp_decls_1 | [Symbol (l, vname); sexp] -> if SMap.mem vname pending_decls then let decl_loc = SMap.find vname pending_decls in - let v = ({file = l.file; - line = l.line; - column = l.column; - docstr = String.concat "\n" [decl_loc.docstr; - l.docstr]}, - vname) in + let v = + let open Source.Location in + ({file = l.file; + line = l.line; + column = l.column; + docstr = String.concat "\n" [decl_loc.docstr; + l.docstr]}, + vname) + in let pending_decls = SMap.remove vname pending_decls in let pending_defs = ((v, sexp) :: pending_defs) in if SMap.is_empty pending_decls then
===================================== src/eval.ml ===================================== @@ -678,7 +678,7 @@ and print_trace title trace default = (* Now eval trace and elab trace are the same *) let print_trace = (fun type_name type_string type_loc i expr -> (* Print location info *) - print_string (" [" ^ (loc_string (type_loc expr)) ^ "] "); + print_string (" [" ^ (Source.Location.to_string (type_loc expr)) ^ "] ");
(* Print call trace visualization *) Fmt.print_ct_tree i; print_string "+- "; @@ -969,8 +969,7 @@ let test_info loc _depth args_val = match args_val with | _ -> error loc "Test.info takes two String as argument"
let test_location loc _depth args_val = match args_val with - | [_] -> Vstring (loc.file ^ ":" ^ string_of_int loc.line - ^ ":" ^ string_of_int loc.column) + | [_] -> Vstring (Source.Location.to_string loc) | _ -> error loc "Test.location takes a Unit as argument"
let test_true loc _depth args_val = match args_val with
===================================== src/log.ml ===================================== @@ -106,11 +106,6 @@ let mkEntry level ?kind ?section ?print_action ?loc msg = let log_push (entry : log_entry) = typer_log := entry::(!typer_log)
-let string_of_location (loc : location) = - (loc.file ^ ":" - ^ string_of_int loc.line ^ ":" - ^ string_of_int loc.column ^ ":") - let maybe_color_string color_opt str = match color_opt with | Some color -> Fmt.color_string color str @@ -119,7 +114,7 @@ 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) + (option_default "" (option_map Source.Location.to_string loc) ^ maybe_color_string color (option_default (string_of_level level) kind) ^ ":" ^ option_default "" (option_map parens section) ^ " " ^ msg)
===================================== src/opslexp.ml ===================================== @@ -1226,7 +1226,7 @@ let erase_type lctx lxp = Log.log_fatal ~print_action:(fun () -> IMap.iter (fun i (_, t, _, (l, n)) -> - print_endline ("\t" ^ (Log.string_of_location l) + print_endline ("\t" ^ (Source.Location.to_string l) ^ " ?" ^ (U.option_default "" n) ^ "[" ^ (string_of_int i) ^ "] : " ^ (lexp_string t)) ) mvs)
===================================== src/positivity.ml ===================================== @@ -0,0 +1,134 @@ +(* Copyright (C) 2021 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * Keywords: languages, lisp, dependent types. + * + * 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/. *) + +(* Positivity is a syntactic property of type which prevent a common source of + contradiction. In a nutshell, it means that a type T doesn't contain an arrow + with T as its domain, or another inductive type with T as a parameter. How + could we use this to create a contradiction? Take this definition for + example. + + type Evil + | make-evil (Evil -> Void); + + If this were allowed we could write this function. + + innocent-function : Evil -> Void; + innocent-function evil = + case evil + | make-evil e => e evil + + Finally, we create a value of type Void. + + what-have-we-done? : Void; + what-have-we-done? = innocent-function (make-evil innocent-function) + + We created an infinite loop. If our function looks innocuous enough, it's + because we hid the loop inside our mischievous make-evil constructor. + Checking inductive types for positivity prevents us from creating such + constructors. *) + +open Lexp +open Util + +(* Computes if the judgement x ∉ fv(τ) holds. *) +let 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.lexp_lexp' 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) + (* + * x ∉ fv(e⃗) + * ────────────── + * x ⊢ x e⃗ pos + *) + -> begin + match Lexp.lexp_lexp' (Lexp.nosusp f) with + | Lexp.Var (_, index') when Int.equal index index' + -> List.for_all (fun (_, arg) -> absent index arg) args + | _ + (* If x ∈ fv(f e⃗), but f ≠ x, then x must occur in e⃗. *) + -> 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.Lambda (_, _, _, e) -> positive index e + + | 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.Let _ | Lexp.Sort _ | Lexp.SortLevel _ + (* There are no rules that have these synctactic forms as a conclusion. *) + -> false + + | Lexp.Builtin _ | Lexp.Imm _ + -> failwith "must never happen since we already know that x ∈ fv(e)" + + | Lexp.Metavar _ + -> failwith "positivity must be checked after metavariables instanciation" + +and positive_in_constructor index vs = + match vs with + | [] -> true + | (_, _, tau) :: vs + -> positive index tau && positive_in_constructor (index + 1) vs
===================================== src/prelexer.ml ===================================== @@ -110,26 +110,38 @@ let rec prelex (source : #Source.t) ln ctx acc (doc : string) let rec prestring cp chars = match source#next_char with | None | Some ('\n') - -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + -> let location = + let open Source.Location in + {file=source#file_name; line=ln; column=cpos; docstr=doc} + in prelexer_error location "Unterminated string"; nextline ctx (Prestring (location, "") :: acc) ""
| Some ('"') - -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + -> let location = + let open Source.Location in + {file=source#file_name; line=ln; column=cpos; docstr=doc} + in let pretoken = Prestring (location, string_implode (List.rev chars)) in nexttok (cp + 1) (pretoken :: acc) ""
| Some ('\') -> (match source#next_char with | None | Some ('\n') - -> let location = {file=source#file_name; line=ln; column=cp; docstr=doc} in + -> let location = + let open Source.Location in + {file=source#file_name; line=ln; column=cp; docstr=doc} + in prelexer_error location "Unterminated escape sequence"; nextline ctx (Prestring (location, "") :: acc) "" | Some ('t') -> prestring (cp + 2) ('\t' :: chars) | Some ('n') -> prestring (cp + 2) ('\n' :: chars) | Some ('r') -> prestring (cp + 2) ('\r' :: chars) | Some ('u') - -> let location = {file=source#file_name; line=ln; column=cp; docstr=doc} in + -> let location = + let open Source.Location in + {file=source#file_name; line=ln; column=cp; docstr=doc} + in prelexer_error location "Unimplemented unicode escape"; prestring (cp + 2) chars | Some (c) -> prestring (cp + 2) (c :: chars)) @@ -161,12 +173,18 @@ let rec prelex (source : #Source.t) ln ctx acc (doc : string) let rec pretok cp = match source#peek_char with | None | Some (' ' | '\t' | '%' | '"' | '{' | '}') - -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + -> let location = + let open Source.Location in + {file=source#file_name; line=ln; column=cpos; docstr=doc} + in let text = source#slice_from_offset start_offset in nexttok cp (Pretoken (location, text) :: acc) ""
| Some ('\n') - -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + -> let location = + let open Source.Location in + {file=source#file_name; line=ln; column=cpos; docstr=doc} + in let text = source#slice_from_offset start_offset in source#advance; nextline ctx (Pretoken (location, text) :: acc) "" @@ -176,7 +194,10 @@ let rec prelex (source : #Source.t) ln ctx acc (doc : string) (match source#next_char with | Some (char) -> pretok (1 + inc_cp cp char) | None - -> let location = {file=source#file_name; line=ln; column=cpos; docstr=doc} in + -> let location = + let open Source.Location in + {file=source#file_name; line=ln; column=cpos; docstr=doc} + in source#advance; let text = source#slice_from_offset start_offset in prelexer_error location ("Unterminated escape sequence in: " ^ text);
===================================== src/sexp.ml ===================================== @@ -81,6 +81,7 @@ let rec sexp_location (s : sexp) : location = let rec sexp_string ?(print_locations = false) sexp = (if print_locations then + let open Source.Location in let {file; line; column; _} = sexp_location sexp in Printf.sprintf "#;("%s" %d %d) " file line column else "")
===================================== src/source.ml ===================================== @@ -18,13 +18,15 @@ * 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 location = Util.location - module Location = struct - type t = location + type t = {file : string; line : int; column : int; docstr : string} + + let dummy = {file = ""; line = 0; column = 0; docstr = ""} + + let to_string ({file; line; column; _} : t) : string = + Printf.sprintf "%s:%d:%d" file line column
let equal (l : t) (r : t) = - let open Util in let {file = l_file; line = l_line; column = l_column; docstr = l_doc} = l in let {file = r_file; line = r_line; column = r_column; docstr = r_doc} = r in String.equal l_file r_file
===================================== src/util.ml ===================================== @@ -38,8 +38,8 @@ module IMap = UPDATABLE(Map.Make(Int))
type charpos = int type bytepos = int -type location = { file : string; line : int; column : charpos; docstr : string; } -let dummy_location = {file=""; line=0; column=0; docstr=""} +type location = Source.Location.t +let dummy_location = Source.Location.dummy
(*************** DeBruijn indices for variables *********************)
@@ -63,12 +63,6 @@ let get_vname_name vname = | Some n -> n | _ -> "" (* FIXME: Replace with dummy_name ? *)
-(* print debug info *) -let loc_string loc = - "Ln " ^ (Fmt.ralign_int loc.line 3) ^ ", cl " ^ (Fmt.ralign_int loc.column 3) - -let loc_print loc = print_string (loc_string loc) - let string_implode chars = String.concat "" (List.map (String.make 1) chars) let string_sub str b e = String.sub str b (e - b)
===================================== tests/dune ===================================== @@ -9,6 +9,7 @@ lexp_test lexer_test macro_test + positivity_test sexp_test unify_test) (deps (alias %{project_root}/btl/typer_stdlib))
===================================== tests/lexer_test.ml ===================================== @@ -66,7 +66,7 @@ let test_lex name pretokens expected = in add_test "LEXER" name lex
-let l : location = +let l : Source.Location.t = {file = "test.typer"; line = 1; column = 1; docstr = ""}
let () =
===================================== tests/positivity_test.ml ===================================== @@ -0,0 +1,118 @@ +(* Copyright (C) 2021 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * Keywords: languages, lisp, dependent types. + * + * 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 Typerlib +open Utest_lib + +open Lexp +open Positivity +open Util + +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); + let decls = List.flatten decls in + List.map (fun (vname, lexp, _) -> print_lexp lexp; (vname, lexp)) 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 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/-/compare/965cc049dc522e23b84f3a11a43075934...