Octobre 2019 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][master] Allow "impredicative" universe polymorphism
by Stefan 22 Oct '19

22 Oct '19

Stefan pushed to branch master at Stefan / Typer Commits: 634f6df0 by Stefan Monnier at 2019-10-22T21:58:25Z Allow "impredicative" universe polymorphism * samples/hurkens.typer (𝓅): Make it universe-polymorphic. * src/elab.ml (infer_level): New function. (sform_type): Use it. * src/log.ml (log_fatal): Set print_at_log before calling log_msg so the message is printed before raising the exception, otherwise it's lost. * src/opslexp.ml (deep_universe_poly): New const. (sort_compose): Add one more context for k2. Fix k2 scoping. Obey deep_universe_poly. - - - - - 6 changed files: - samples/hurkens.typer - src/builtin.ml - src/elab.ml - src/lexp.ml - src/log.ml - src/opslexp.ml Changes: ===================================== samples/hurkens.typer ===================================== @@ -12,19 +12,21 @@ %%% Code: +* = Type_ (s z); +□ = Type_ (s (s z)); + ⊥ : Type; ⊥ = (p : Type) ≡> p; ¬ : (ℓ : TypeLevel) ≡> Type_ ℓ -> Type_ ℓ; -¬ t = t -> ⊥; - -* = Type; -□ = Type1; +¬ t = t -> ⊥ ; %% 𝓅 is the "powerset". -%% 𝓅 S = (S -> *); FIXME: internal error! -𝓅 : □ -> □; -𝓅 (S : □) = (S -> *); +%% 𝓅 S = (S -> *); +𝓅 : (ℓ : TypeLevel) => Type_ (s ℓ) -> Type_ (s ℓ); +%% FIXME: `?` instead of `ℓ` below leads to a type error because it +%% infers a type `Type_ (s (ℓ ∪ ℓ))` instead of `Type_ (s ℓ)` :-( +𝓅 S = (S -> Type_ ℓ); 𝓅𝓅 S = 𝓅 (𝓅 S); %%%% A "powerful" universe (U, σ, τ). ===================================== src/builtin.ml ===================================== @@ -1,6 +1,6 @@ (* builtin.ml --- Infrastructure to define built-in primitives * - * Copyright (C) 2016-2018 Free Software Foundation, Inc. + * Copyright (C) 2016-2019 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. ===================================== src/elab.ml ===================================== @@ -1504,7 +1504,7 @@ let rec sform_lambda kind ctx loc sargs ot = * so auto-add a corresponding Lambda wrapper! * FIXME: This should be moved to a macro. *) -> (* FIXME: Here we end up adding a local variable `v` whose - * name is lot lexically present, so there's a risk of + * name is not lexically present, so there's a risk of * name capture. We should make those vars anonymous? *) let nctx = ectx_extend ctx v Variable lt1 in (* FIXME: Don't go back to sform_lambda, but use an internal @@ -1556,6 +1556,16 @@ let sform_letin ctx loc sargs ot = match sargs with | _ -> sexp_error loc "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc +let rec infer_level ctx se : lexp = + match se with + | Symbol (_, "z") -> mkSortLevel SLz + | Symbol _ -> check se type_level ctx + | Node (Symbol (_, "s"), [se]) + -> mkSortLevel (SLsucc (infer_level ctx se)) + | _ -> let l = (sexp_location se) in + (sexp_error l ("Unrecognized TypeLevel: " ^ sexp_string se); + newMetavar (ectx_to_lctx ctx) dummy_scope_level (l, None) type_level) + (* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) * But it would be less efficient (such a lambda can't be passed as argument @@ -1564,11 +1574,11 @@ let sform_letin ctx loc sargs ot = match sargs with * allow such a lambda. *) let sform_type ctx loc sargs ot = match sargs with - | [l] -> let l, _ = infer l ctx in - (mkSort (loc, Stype l), - Inferred (mkSort (loc, Stype (SortLevel (mkSLsucc l))))) - | _ -> sexp_error loc "##Type_ expects one argument"; - sform_dummy_ret ctx loc + | [se] -> let l = infer_level ctx se in + (mkSort (loc, Stype l), + Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l))))) + | _ -> (sexp_error loc "##Type_ expects one argument"; + sform_dummy_ret ctx loc) let sform_debruijn ctx loc sargs ot = match sargs with ===================================== src/lexp.ml ===================================== @@ -218,7 +218,7 @@ let mkSLlub' (e1, e2) = match (e1, e2) with let mkSLsucc e = match e with | SortLevel _ | Var _ | Metavar _ | Susp _ -> SLsucc e - | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level" + | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level " (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. ===================================== src/log.ml ===================================== @@ -159,7 +159,7 @@ let set_typer_log_level_str str = with _ -> set_typer_log_level (level_of_string str) -let increment_log_level () = +let increment_log_level () : unit = typer_log_config.level |> int_of_level |> (+) 1 @@ -189,6 +189,7 @@ exception Stop_Compilation of string let stop_compilation s = raise (Stop_Compilation s) let log_fatal ?section ?print_action ?loc m = + typer_log_config.print_at_log <- true; log_msg Fatal ~kind:"[X] Fatal " ?section ?print_action ?loc m; internal_error "Compiler Fatal Error" let log_error = log_msg Error ?kind:None ===================================== src/opslexp.ml ===================================== @@ -44,9 +44,14 @@ let warning_tc = Log.log_warning ~section:"TC" (* `conv_erase` is supposed to be safe according to the ICC papers. *) let conv_erase = true (* Makes conv ignore erased terms. *) -(* The safety of `impredicative_erase` is unknown. But I like the idea. *) +(* `impredicative_erase` is inconsistent: as shown in samples/hurkens.typer + * it allows the definition of an inf-looping expression of type ⊥. *) let impredicative_erase = true (* Allows erasable args to be impredicative. *) +(* The safety of `deep_universe_poly` is unknown. + * But I also like the idea. *) +let deep_universe_poly = true (* Assume arg is TypeLevel.z when erasable. *) + (* Lexp context *) let lookup_type = DB.lctx_lookup_type @@ -343,19 +348,24 @@ type sort_compose_result | SortK1NotType | SortK2NotType -let sort_compose ctx l ak k1 k2 = +let sort_compose ctx1 ctx2 l ak k1 k2 = (* BEWARE! Technically `k2` can refer to `v`, but this should only happen - * if `v` is a TypeLevel, and in that case sort_compose - * should ignore `k2` and return TypeOmega anyway. *) - let k2 = mkSusp k2 (S.substitute impossible) in - match (lexp_whnf k1 ctx, lexp_whnf k2 ctx) with + * if `v` is a TypeLevel. *) + match (lexp_whnf k1 ctx1, lexp_whnf k2 ctx2) with | (Sort (_, s1), Sort (_, s2)) - (* FIXME: fix scoping of `k2` and `s2`. *) -> (match s1, s2 with | (Stype l1, Stype l2) -> if ak == P.Aerasable && impredicative_erase - then SortResult k2 - else SortResult (mkSort (l, Stype (mkSLlub ctx l1 l2))) + then SortResult (mkSusp k2 (S.substitute impossible)) + else let l2' = (mkSusp l2 (S.substitute impossible)) in + SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2'))) + | (StypeLevel, Stype l2) + when ak == P.Aerasable && deep_universe_poly + (* The safety/soundness of this rule is completely unknown. + * It's pretty powerful, e.g. allows tuples containing + * level-polymorphic functions, and makes impredicative-encoding + * of data types almost(just?) as flexible as inductive types. *) + -> SortResult (mkSusp k2 (S.substitute DB.level0)) | (StypeLevel, Stype _) | (StypeLevel, StypeOmega) (* This might be safe, but I don't think it adds much power. @@ -483,7 +493,7 @@ let rec check'' erased ctx e = -> (let k1 = check_type erased ctx t1 in let nctx = DB.lexp_ctx_cons ctx v Variable t1 in let k2 = check_type (DB.set_sink 1 erased) nctx t2 in - match sort_compose ctx l ak k1 k2 with + match sort_compose ctx nctx l ak k1 k2 with | SortResult k -> k | SortInvalid -> error_tc ~loc:l "Invalid arrow: inner TypelLevel argument"; @@ -805,7 +815,7 @@ let rec get_type ctx e = -> (let k1 = get_type ctx t1 in let nctx = DB.lexp_ctx_cons ctx v Variable t1 in let k2 = get_type nctx t2 in - match sort_compose ctx l ak k1 k2 with + match sort_compose ctx nctx l ak k1 k2 with | SortResult k -> k | _ -> mkSort (l, StypeOmega)) | Lambda (ak, ((l,_) as v), t, e) View it on GitLab: https://gitlab.com/monnier/typer/commit/634f6df0a52c10ba036f99e3cee3f7be47a… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/634f6df0a52c10ba036f99e3cee3f7be47a… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] 2 commits: * src/elab.ml (sform_lambda): Rename the type's var
by Stefan 22 Oct '19

22 Oct '19

Stefan pushed to branch master at Stefan / Typer Commits: 71ec8850 by Stefan Monnier at 2019-10-22T20:41:34Z * src/elab.ml (sform_lambda): Rename the type's var This should fix some deBruijn errors for cases like: x : (y : T1) -> T2 y; x z = e; since the (dependent) type of `e` will use the name `z` rather than `y`. Apparently it doesn't fix all our deBruijn name check errors, tho :-( * sample/hurkens.typer: Unrelated cosmetic changes. - - - - - c3706c38 by Stefan Monnier at 2019-10-22T20:45:23Z Merge branch 'master' of gitlab.com:monnier/typer into trunk - - - - - 2 changed files: - samples/hurkens.typer - src/elab.ml Changes: ===================================== samples/hurkens.typer ===================================== @@ -15,16 +15,16 @@ ⊥ : Type; ⊥ = (p : Type) ≡> p; -¬ : Type -> Type; +¬ : (ℓ : TypeLevel) ≡> Type_ ℓ -> Type_ ℓ; ¬ t = t -> ⊥; * = Type; -\square = Type1; +□ = Type1; %% 𝓅 is the "powerset". %% 𝓅 S = (S -> *); FIXME: internal error! -𝓅 : \square -> \square; -𝓅 (S : \square) = (S -> Type); +𝓅 : □ -> □; +𝓅 (S : □) = (S -> *); 𝓅𝓅 S = 𝓅 (𝓅 S); %%%% A "powerful" universe (U, σ, τ). @@ -38,11 +38,11 @@ %% %% where * is ... -U : \square; -U = (X : \square) ≡> (𝓅𝓅 X -> X) -> 𝓅𝓅 X; % Uses the (▵,□,□) rule! +U : □; +U = (X : □) ≡> (𝓅𝓅 X -> X) -> 𝓅𝓅 X; % Uses the (▵,□,□) rule! τ : 𝓅𝓅 U -> U; -τ t = lambda (X : \square) +τ t = lambda (X : □) ≡> lambda (f : (𝓅𝓅 X) -> X) -> lambda (p : 𝓅 X) -> t (lambda (y : U) -> p (f ((y (X := X) f)))); @@ -91,5 +91,10 @@ boom2 = lambda (p : 𝓅 U) %%boom : ⊥; %%boom = boom1 boom2; +%% Summary: +%% U = (X : □) ≡> (𝓅𝓅 X → X) → 𝓅𝓅 X +%% Δ .. (y : U) = (p : U → *) ≡> σ y p → p (τσ y) +%% wf = (p : U → *) ≡> ((y : U) ≡> σ y p → p y) → p Ω + %%% hurkens.typer ends here. ===================================== src/elab.ml ===================================== @@ -1466,6 +1466,14 @@ let rec sform_lambda kind ctx loc sargs ot = let mklam lt1 olt2 = let nctx = ectx_extend ctx arg Variable lt1 in + let olt2 = match olt2 with + | None -> None + (* Apply a "dummy" substitution which replace #0 with #0 + * in order to account for the fact that `arg` and `v` + * might not be the same name! *) + | Some lt2 + -> let s = S.cons (mkVar (arg, 0)) (S.shift 1) in + Some (mkSusp lt2 s) in let (lbody, alt) = elaborate nctx sbody olt2 in (mkLambda (kind, arg, lt1, lbody), match alt with @@ -1566,7 +1574,7 @@ let sform_debruijn ctx loc sargs ot = match sargs with | [Integer (l,i)] -> if i < 0 || i > get_size ctx then - (sexp_error l "##DeBruijn indiex out of bounds"; + (sexp_error l "##DeBruijn index out of bounds"; sform_dummy_ret ctx loc) else let lxp = mkVar ((loc, None), i) in (lxp, Lazy) View it on GitLab: https://gitlab.com/monnier/typer/compare/b948d4c96126d1eb4796088bc80654647e… -- View it on GitLab: https://gitlab.com/monnier/typer/compare/b948d4c96126d1eb4796088bc80654647e… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][simon-genier] Judge if an expression is positive in a variable.
by Simon Génier 18 Oct '19

18 Oct '19

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(a)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(a)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(a)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(a)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/94b782eff7a934fad1e9823c28a8aad168d… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/94b782eff7a934fad1e9823c28a8aad168d… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch tp/ift6172-2019
by Stefan 18 Oct '19

18 Oct '19

Stefan pushed new branch tp/ift6172-2019 at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/tree/tp/ift6172-2019 You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][simon-genier] [WIP] Judge if an expression is positive in a variable.
by Simon Génier 16 Oct '19

16 Oct '19

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(a)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(a)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(a)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(a)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/99dc3728beee59701f588b777200d20f856… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/99dc3728beee59701f588b777200d20f856… You're receiving this email because of your account on gitlab.com.

2 1

[Git][monnier/typer][simon-genier] Judge if an expression is positive in a variable.
by Simon Génier 16 Oct '19

16 Oct '19

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(a)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(a)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(a)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(a)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/4c2bffb966c03d59e0d3fe710f1db411078… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/4c2bffb966c03d59e0d3fe710f1db411078… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][simon-genier] [WIP] Judge if an expression is positive in a variable.
by Simon Génier 16 Oct '19

16 Oct '19

Simon Génier pushed to branch simon-genier at Stefan / Typer Commits: f7f82cb2 by Simon Génier at 2019-10-16T20:59:07Z [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,38 @@ +(* list.ml --- + * + * Copyright (C) 2019 Free Software Foundation, Inc. + * + * Author: Simon Génier <simon.genier(a)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(a)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(a)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(a)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/f7f82cb2265d395e10cdc9390f6142a7f5d… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/f7f82cb2265d395e10cdc9390f6142a7f5d… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][simon-genier] [WIP] Judge if an expression is positive in a variable.
by Simon Génier 10 Oct '19

10 Oct '19

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(a)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(a)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(a)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(a)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(a)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/b2247a87d0dfd7407e426dfd481c7aa6ae8… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/b2247a87d0dfd7407e426dfd481c7aa6ae8… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][simon-genier] 12 commits: * lexp.ml (lexp): Typo
by Simon Génier 10 Oct '19

10 Oct '19

Simon Génier pushed to branch simon-genier at Stefan / Typer Commits: 25bb77ab by Stefan Monnier at 2019-09-26T20:51:26Z * lexp.ml (lexp): Typo - - - - - 5c7f8365 by Stefan Monnier at 2019-09-26T20:52:00Z Merge remote-tracking branch 'refs/remotes/gitlab/master' into trunk - - - - - 9455fa18 by Jean-Alexandre Barszcz at 2019-10-04T01:46:06Z Extract logging from util.ml - - - - - c1458d9a by Jean-Alexandre Barszcz at 2019-10-04T01:46:06Z Replace typer_unreachable exception with 'failwith' - - - - - 82fa3593 by Jean-Alexandre Barszcz at 2019-10-04T01:46:06Z Refactor logging - - - - - 51251f1f by Jean-Alexandre Barszcz at 2019-10-04T01:46:06Z Add optional color to logging - - - - - 2a2afc56 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Print errors/warnings all at once, after compilation stops - - - - - 09952ed7 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Print the log in default context - - - - - c02e28bc by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Add an option to control the verbosity/logging level - - - - - f41b8bb3 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Always print the log after evaluation If there are warnings (or other messages of lesser priority in the log), we want to print them. Similarly, errors for which we were able to recover might still exist in the log. Regardless of whether compilation has been stopped, we thus print the log. - - - - - b948d4c9 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Print test messages instead of logging them - - - - - a4484eb9 by Simon Génier at 2019-10-11T02:29:36Z [WIP] Judge if an expression is positive in a variable. - - - - - 23 changed files: - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml - + src/list.ml - + src/log.ml - src/opslexp.ml - + src/option.ml - src/pexp.ml - + src/positivity.ml - src/prelexer.ml - src/sexp.ml - src/unification.ml - src/util.ml - + tests/positivity_test.ml - + tests/select.ml - tests/utest_lib.ml Changes: ===================================== src/REPL.ml ===================================== @@ -63,8 +63,16 @@ let print_input_line i = ralign_print_int i 2; print_string "] >> " -let ieval_error loc msg = - msg_error "IEVAL" loc msg +let ieval_error = Log.log_error ~section:"IEVAL" + +let print_and_clear_log () = + if (not Log.typer_log_config.print_at_log) then + Log.print_and_clear_log () + +let handle_stopped_compilation msg = + print_and_clear_log (); + print_string msg; print_newline (); + flush stdout (* Read stdin for input. Returns only when the last char is ';' * We can use '%' to prevent parsing @@ -207,7 +215,7 @@ let readfiles files (i, lctx, rctx) prt = (List.iter (print_eval_result i) ret; (i + 1, lctx, rctx)) with Sys_error _ -> ( - ieval_error dloc ("file \"" ^ file ^ "\" does not exist."); + ieval_error ("file \"" ^ file ^ "\" does not exist."); (i, lctx, rctx)) ) (i, lctx, rctx) files @@ -231,8 +239,8 @@ let rec repl i clxp rctx = let (i, clxp, rctx) = try readfiles args (i, clxp, rctx) false - with Stop_Compilation s -> - (print_string s; (i,clxp,rctx)) + with Log.Stop_Compilation msg -> + (handle_stopped_compilation msg; (i,clxp,rctx)) in repl clxp rctx; | "%who"::args | "%w"::args -> ( @@ -247,18 +255,25 @@ let rec repl i clxp rctx = repl clxp rctx) | cmd::_ -> - ieval_error dloc (" \"" ^ cmd ^ "\" is not a correct repl command"); + ieval_error (" \"" ^ cmd ^ "\" is not a correct repl command"); repl clxp rctx | _ -> repl clxp rctx) (* eval input *) - | _ -> ( + | _ -> try let (ret, clxp, rctx) = (ieval_string ipt clxp rctx) in + print_and_clear_log (); List.iter (print_eval_result i) ret; repl clxp rctx - with e -> match e with - | Stop_Compilation msg -> (print_string msg; repl clxp rctx) - | _ -> catch_error (); repl clxp rctx) + with + | Log.Stop_Compilation msg -> + (handle_stopped_compilation msg; repl clxp rctx) + | Log.Internal_error msg -> + (handle_stopped_compilation ("Internal error: " ^ msg); + repl clxp rctx) + | Log.User_error msg -> + (handle_stopped_compilation ("Fatal user error: " ^ msg); + repl clxp rctx) let arg_files = ref [] @@ -266,6 +281,9 @@ let arg_files = ref [] (* ./typer [options] files *) let arg_defs = [ ("--batch", Arg.Set arg_batch, "Don't run the interactive loop"); + ("--verbosity", + Arg.String Log.set_typer_log_level_str, "Set the logging level"); + ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity"); (* ("--debug", Arg.Set arg_debug, "Print the Elexp representation") *) (*"-I", Arg.String (fun f -> searchpath := f::!searchpath), @@ -287,8 +305,19 @@ let main () = print_string (make_sep '-'); flush stdout); - let (i, ectx, rctx) = readfiles (List.rev !arg_files) (1, ectx, rctx) - (not !arg_batch) in + let (i, ectx, rctx) = ( + try + let res = + readfiles (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch) in + print_and_clear_log (); res + with + | Log.Stop_Compilation msg -> + handle_stopped_compilation msg; exit 1 + | Log.Internal_error msg -> + handle_stopped_compilation ("Internal error: " ^ msg); exit 1 + | Log.User_error msg -> + handle_stopped_compilation ("Fatal user error: " ^ msg); exit 1 + ) in flush stdout; ===================================== src/builtin.ml ===================================== @@ -64,8 +64,9 @@ open Lexp module DB = Debruijn module E = Env -let error loc msg = msg_error "BUILT-IN" loc msg; raise (internal_error msg) -let warning loc msg = msg_warning "BUILT-IN" loc msg +let log_raise_error ?loc msg = + Log.log_error ~section:"BUILT-IN" ?loc msg; + Log.internal_error msg let predef_names = [ "cons"; (* FIXME: Should be used but isn't! *) @@ -87,7 +88,7 @@ let get_predef (name: string) (ctx: DB.elab_context) : lexp = try let r = (DB.get_size ctx) - !builtin_size - 0 in let p = SMap.find name (!predef_map) in mkSusp p (S.shift r) - with Not_found -> error dummy_location ("\""^ name ^ "\" was not predefined") + with Not_found -> log_raise_error ("\""^ name ^ "\" was not predefined") let set_predef name lexp = predef_map := SMap.add name lexp (!predef_map) @@ -131,9 +132,9 @@ let v2o_list v = match v with | E.Vcons ((_, "cons"), [hd; tl]) -> v2o_list (hd::acc) tl | E.Vcons ((_, "nil"), []) -> List.rev acc - | _ -> print_string (E.value_name v); print_string "\n"; - E.value_print v; - error dloc "List conversion failure'" in + | _ -> log_raise_error ~loc:(E.value_location v) ( + "Failed to convert the " ^ E.value_name v ^ " with value :\n" + ^ E.value_string v ^ "\n to a list.") in v2o_list [] v (* Map of lexp builtin elements accessible via (## <name>). *) ===================================== src/debruijn.ml ===================================== @@ -42,8 +42,7 @@ open Fmt module S = Subst -let error l m = msg_error "DEBRUIJN" l m; internal_error m -let warning = msg_warning "DEBRUIJN" +let fatal = Log.log_fatal ~section:"DEBRUIJN" (* Handling scoping/bindings is always tricky. So it's always important * to keep in mind for *every* expression which is its context. @@ -316,17 +315,17 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = | (((_, Some name), _, _), Some ename) -> (* Check if names match *) if not (ename = name) then - (print_lexp_ctx ctx; - error loc ("DeBruijn index " - ^ string_of_int dbi - ^ " refers to wrong name. " - ^ "Expected: `" ^ ename - ^ "` got `" ^ name ^ "`")) + fatal ~loc ~print_action:(fun _ -> + print_lexp_ctx ctx; print_newline ()) + ("DeBruijn index " ^ string_of_int dbi + ^ " refers to wrong name. " + ^ "Expected: `" ^ ename + ^ "` got `" ^ name ^ "`") | _ -> () in ret) with - Not_found -> error loc ("DeBruijn index " + Not_found -> fatal ~loc ("DeBruijn index " ^ string_of_int dbi ^ " of `" ^ maybename oename ^ "` out of bounds!") @@ -366,7 +365,7 @@ let rec lctx_view lctx = | _ -> CVfix (defs, lctx) in loop 2 lctx [(loname, def, t)] | Myers.Mcons ((_, LetDef (o, def), _), _, _, _) when o > 1 - -> U.internal_error "Unexpected lexp_context shape!" + -> fatal "Unexpected lexp_context shape!" | Myers.Mcons ((loname, odef, t), lctx, _, _) -> CVlet (loname, odef, t, lctx) ===================================== src/elab.ml ===================================== @@ -69,21 +69,28 @@ let btl_folder = try Sys.getenv "TYPER_BUILTINS" with Not_found -> "./btl" -let warning = msg_warning "ELAB" -let error = msg_error "ELAB" -let fatal = msg_fatal "ELAB" - -(* Print Lexp name followed by the lexp in itself, finally throw an exception *) -let debug_message error_type type_name type_string loc expr message = - EV.debug_messages error_type loc - message [ - (type_name expr) ^ ": " ^ (type_string expr); - ] - -let lexp_fatal = debug_message fatal lexp_name lexp_string -let lexp_warning = debug_message warning lexp_name lexp_string -let lexp_error = debug_message error lexp_name lexp_string -let value_fatal = debug_message fatal value_name value_string +let fatal = Log.log_fatal ~section:"ELAB" +let error = Log.log_error ~section:"ELAB" +let warning = Log.log_warning ~section:"ELAB" +let info = Log.log_info ~section:"ELAB" + +let indent_line str = + " > " ^ str +let print_indent_line str = + print_endline (indent_line str) +let print_details to_name to_str elem = + print_indent_line ((to_name elem) ^ ": " ^ (to_str elem)) +let lexp_print_details lexp () = + print_details lexp_name lexp_string lexp +let value_print_details value () = + print_details value_name value_string value + +let lexp_error loc lexp = + error ~loc ~print_action:(lexp_print_details lexp) +let lexp_fatal loc lexp = + fatal ~loc ~print_action:(lexp_print_details lexp) +let value_fatal loc value = + fatal ~loc ~print_action:(value_print_details value) (** Type info returned by elaboration. *) type sform_type = @@ -116,9 +123,9 @@ let sform_default_ectx = ref empty_elab_context let elab_check_sort (ctx : elab_context) lsort var ltp = match (try OL.lexp_whnf lsort (ectx_to_lctx ctx) with e -> - print_string "Exception during whnf of "; - lexp_print lsort; - print_string "\n"; + info ~print_action:(fun _ -> lexp_print lsort; print_newline ()) + ~loc:(lexp_location lsort) + "Exception during whnf of sort:"; raise e) with | Sort (_, _) -> () (* All clear! *) | _ -> let lexp_string e = lexp_string (L.clean e) in @@ -134,15 +141,19 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = let elab_check_proper_type (ctx : elab_context) ltp var = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp with e -> match e with - | Stop_Compilation _ -> raise e - | _ -> print_string "Exception while checking type `"; - lexp_print ltp; - (match var with - | (_, None) -> () - | (_, Some name) - -> print_string ("` of var `" ^ name ^"`\n")); - print_lexp_ctx (ectx_to_lctx ctx); - raise e + | Log.Stop_Compilation _ -> raise e + | _ -> + info + ~print_action:(fun _ -> + print_lexp_ctx (ectx_to_lctx ctx); print_newline () + ) + ~loc:(lexp_location ltp) + ("Exception while checking type `" ^ (lexp_string ltp) ^ "`" + ^ (match var with + | (_, None) -> "" + | (_, Some name) + -> " of var `" ^ name ^ "`")); + raise e let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in @@ -151,30 +162,37 @@ let elab_check_def (ctx : elab_context) var lxp ltype = let lexp_string e = lexp_string (L.clean e) in let ltype' = try OL.check lctx lxp with e -> match e with - (* lexp_error is fatal but Stop_Compilation isn't *) - | Stop_Compilation _ -> raise e - | _ -> lexp_error loc lxp "Error while type-checking"; + | Log.Stop_Compilation _ -> raise e + | _ -> + info + ~print_action:(fun _ -> + lexp_print_details lxp (); print_lexp_ctx (ectx_to_lctx ctx); - raise e in + print_newline () + ) + ~loc + "Error while type-checking"; + raise e in if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' - with e - -> print_string ("Exception while conversion-checking types:\n"); - lexp_print ltype; - print_string (" and "); - lexp_print ltype'; - print_string ("\n"); - lexp_error loc lxp - ("Exception while conversion-checking types " - ^ lexp_string ltype ^ " and " ^ lexp_string ltype'); - raise e) + with e -> + info ~print_action:(lexp_print_details lxp) + ~loc + ("Exception while conversion-checking types: " + ^ lexp_string ltype ^ " and " ^ lexp_string ltype'); + raise e) then elab_check_proper_type ctx ltype var else - (EV.debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [ - (match var with (_, Some n) -> n | _ -> "<anon>") - ^ " = " ^ lexp_string lxp ^ " !: " ^ lexp_string ltype; - " because"; - lexp_string ltype' ^ " != " ^ lexp_string ltype]) + fatal + ~print_action:(fun _ -> + List.iter print_indent_line [ + (match var with (_, Some n) -> n | _ -> "<anon>") + ^ " = " ^ lexp_string lxp ^ " !: " ^ lexp_string ltype; + " because"; + lexp_string ltype' ^ " != " ^ lexp_string ltype + ]) + ~loc + "Type check error: ¡¡ctx_define error!!" let ctx_extend (ctx: elab_context) (var : vname) def ltype = elab_check_proper_type ctx ltype var; @@ -450,7 +468,7 @@ let rec elaborate ctx se ot = and infer (p : sexp) (ctx : elab_context): lexp * ltype = match elaborate ctx p None with - | (_, Checked) -> fatal (sexp_location p) "`infer` got Checked!" + | (_, Checked) -> fatal ~loc:(sexp_location p) "`infer` got Checked!" | (e, Lazy) -> (e, OL.get_type (ectx_to_lctx ctx) e) | (e, Inferred t) -> (e, t) @@ -609,7 +627,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let pat_string p = sexp_string (pexp_u_pat p) in let uniqueness_warn pat = - warning (pexp_pat_location pat) + warning ~loc:(pexp_pat_location pat) ("Pattern " ^ pat_string pat ^ " is a duplicate. It will override previous pattern.") in @@ -920,7 +938,11 @@ and lexp_eval ectx e = ^ track_fv rctx (ectx_to_lctx ectx) e); try EV.eval ee rctx - with exc -> EV.print_eval_trace None; raise exc + with exc -> + let eval_trace = fst (EV.get_trace ()) in + info ~print_action:(fun _ -> EV.print_eval_trace (Some eval_trace)) + "Exception happened during evaluation:"; + raise exc and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option) : value_type = @@ -954,11 +976,11 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp = | Vcommand cmd -> (match (cmd ()) with | Vsexp (sexp) -> sexp - | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a IO sexp")) - | _ -> fatal loc ("Macro `" ^ mname ^ "` should return an IO") + | _ -> fatal ~loc ("Macro `" ^ mname ^ "` should return a IO sexp")) + | _ -> fatal ~loc ("Macro `" ^ mname ^ "` should return an IO") with e -> - fatal loc ("Macro `" ^ mname ^ "` not found") + fatal ~loc ("Macro `" ^ mname ^ "` not found") and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) @@ -981,7 +1003,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) let d = (v', LetDef (i + 1, e), t) in (IMap.add i ((l, Some vname), e, t) map, (grm, ec, Myers.set_nth i d lc, sl)) - | _ -> U.internal_error "Defining same slot!") + | _ -> Log.internal_error "Defining same slot!") defs (IMap.empty, nctx) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in decls, ctx_define_rec ectx decls @@ -1024,8 +1046,8 @@ and lexp_decls_1 let rec lexp_decls_1 sdecls ectx nctx pending_decls pending_defs = match sdecls with | [] -> (if not (SMap.is_empty pending_decls) then - let (s, l) = SMap.choose pending_decls in - error l ("Variable `" ^ s ^ "` declared but not defined!") + let (s, loc) = SMap.choose pending_decls in + error ~loc ("Variable `" ^ s ^ "` declared but not defined!") else assert (pending_defs == [])); [], [], nctx @@ -1037,22 +1059,22 @@ and lexp_decls_1 -> lexp_decls_1 (List.append sdecls' sdecls) ectx nctx pending_decls pending_defs - | Node (Symbol (l, "_:_"), args) :: sdecls + | Node (Symbol (loc, "_:_"), args) :: sdecls (* FIXME: Move this to a "special form"! *) -> (match args with - | [Symbol (l, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (l, Some vname) in + | [Symbol (loc, vname); stp] + -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) let pt_idx = senv_lookup vname nctx in (* Take the previous type annotation. *) let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) - | _ -> U.internal_error "Var not found at its index!" in + | _ -> Log.internal_error "Var not found at its index!" in (* Unify it with the new one. *) let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with | (None | Some (_::_)) - -> lexp_error l ltp + -> lexp_error loc ltp ("New type annotation `" ^ lexp_string ltp ^ "` incompatible with previous `" ^ lexp_string pt ^ "`") @@ -1060,13 +1082,13 @@ and lexp_decls_1 lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else if List.exists (fun ((_, vname'), _) -> vname = vname') pending_defs then - (error l ("Variable `" ^ vname ^ "` already defined!"); + (error ~loc ("Variable `" ^ vname ^ "` already defined!"); lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) else lexp_decls_1 sdecls ectx - (ectx_extend nctx (l, Some vname) ForwardRef ltp) - (SMap.add vname l pending_decls) + (ectx_extend nctx (loc, Some vname) ForwardRef ltp) + (SMap.add vname loc pending_decls) pending_defs - | _ -> error l "Invalid type declaration syntax"; + | _ -> error ~loc "Invalid type declaration syntax"; lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) | Node (Symbol (l, "_=_") as head, args) :: sdecls @@ -1102,7 +1124,7 @@ and lexp_decls_1 lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else - (error l ("`" ^ vname ^ "` defined but not declared!"); + (error ~loc:l ("`" ^ vname ^ "` defined but not declared!"); lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) | [Node (Symbol s, args) as d; body] @@ -1114,7 +1136,7 @@ and lexp_decls_1 :: sdecls) ectx nctx pending_decls pending_defs - | _ -> error l "Invalid definition syntax"; + | _ -> error ~loc:l "Invalid definition syntax"; lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) | Node (Symbol (l, "define-operator"), args) :: sdecls @@ -1129,12 +1151,12 @@ and lexp_decls_1 pending_decls pending_defs | sexp :: sdecls - -> error (sexp_location sexp) "Invalid declaration syntax"; + -> error ~loc:(sexp_location sexp) "Invalid declaration syntax"; lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in (EV.set_getenv nctx; let res = lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in - (stop_on_error (); res)) + (Log.stop_on_error (); res)) and lexp_p_decls (sdecls : sexp list) (ctx : elab_context) : ((vname * lexp * ltype) list list * elab_context) = @@ -1143,14 +1165,14 @@ and lexp_p_decls (sdecls : sexp list) (ctx : elab_context) | _ -> let decls, sdecls, nctx = lexp_decls_1 sdecls ctx ctx SMap.empty [] in let declss, nnctx = lexp_p_decls sdecls nctx in decls :: declss, nnctx in - let res = impl sdecls ctx in (stop_on_error (); res) + let res = impl sdecls ctx in (Log.stop_on_error (); res) and lexp_parse_all (p: sexp list) (ctx: elab_context) : lexp list = let res = List.map (fun pe -> let e, _ = infer pe ctx in e) p in - (stop_on_error (); res) + (Log.stop_on_error (); res) and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = - let e, _ = infer e ctx in (stop_on_error (); e) + let e, _ = infer e ctx in (Log.stop_on_error (); e) (* -------------------------------------------------------------------------- * Special forms implementation @@ -1166,17 +1188,17 @@ and sform_new_attribute ctx loc sargs ot = OL.lexp_close (ectx_to_lctx ctx) ltp, Some AttributeMap.empty), Lazy) - | _ -> fatal loc "new-attribute expects a single Type argument" + | _ -> fatal ~loc "new-attribute expects a single Type argument" and sform_add_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in let table, var, attr = match List.map (lexp_parse_sexp ctx) sargs with | [table; Var((_, Some name), idx); attr] -> table, (n - idx, name), attr - | _ -> fatal loc "add-attribute expects 3 arguments (table; var; attr)" in + | _ -> fatal ~loc "add-attribute expects 3 arguments (table; var; attr)" in let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map, attr_type - | _ -> fatal loc "add-attribute expects a table as first argument" in + | _ -> fatal ~loc "add-attribute expects a table as first argument" in (* FIXME: Type check (attr: type == attr_type) *) let attr' = OL.lexp_close (ectx_to_lctx ctx) attr in @@ -1188,11 +1210,11 @@ and get_attribute ctx loc largs = let ctx_n = get_size ctx in let table, var = match largs with | [table; Var((_, Some name), idx)] -> table, (ctx_n - idx, name) - | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in + | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in let map = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map - | _ -> fatal loc "get-attribute expects a table as first argument" in + | _ -> fatal ~loc "get-attribute expects a table as first argument" in try Some (AttributeMap.find var map) with Not_found -> None @@ -1206,7 +1228,7 @@ and sform_has_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in let table, var = match List.map (lexp_parse_sexp ctx) sargs with | [table; Var((_, Some name), idx)] -> table, (n - idx, name) - | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in + | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map, attr_type @@ -1220,9 +1242,9 @@ and sform_declexpr ctx loc sargs ot = | [Var((_, vn), vi)] -> (match DB.env_lookup_expr ctx ((loc, vn), vi) with | Some lxp -> (lxp, Lazy) - | None -> error loc "no expr available"; + | None -> error ~loc "no expr available"; sform_dummy_ret ctx loc) - | _ -> error loc "declexpr expects one argument"; + | _ -> error ~loc "declexpr expects one argument"; sform_dummy_ret ctx loc @@ -1230,7 +1252,7 @@ let sform_decltype ctx loc sargs ot = match List.map (lexp_parse_sexp ctx) sargs with | [Var((_, vn), vi)] -> (DB.env_lookup_type ctx ((loc, vn), vi), Lazy) - | _ -> error loc "decltype expects one argument"; + | _ -> error ~loc "decltype expects one argument"; sform_dummy_ret ctx loc let builtin_value_types : ltype option SMap.t ref = ref SMap.empty @@ -1246,13 +1268,13 @@ let sform_built_in ctx loc sargs ot = sexp_error loc ("Unknown built-in `" ^ name ^ "`"); BI.add_builtin_cst name bi; (bi, Checked) - | None -> error loc "Built-in's type not provided by context!"; + | None -> error ~loc "Built-in's type not provided by context!"; sform_dummy_ret ctx loc) - | true, _ -> error loc "Wrong Usage of `Built-in`"; + | true, _ -> error ~loc "Wrong Usage of `Built-in`"; sform_dummy_ret ctx loc - | false, _ -> error loc "Use of `Built-in` in user code"; + | false, _ -> error ~loc "Use of `Built-in` in user code"; sform_dummy_ret ctx loc let sform_datacons ctx loc sargs ot = @@ -1282,8 +1304,9 @@ let elab_typecons_arg arg : (arg_kind * vname * sexp option) = -> (elab_colon_to_ak k, (l, Some name), Some e) | Symbol (l, name) -> (Anormal, (l, Some name), None) - | _ -> sexp_print arg; - (sexp_error (sexp_location arg) "Unrecognized formal arg"); + | _ -> sexp_error ~print_action:(fun _ -> sexp_print arg; print_newline ()) + (sexp_location arg) + "Unrecognized formal arg"; (Anormal, (sexp_location arg, None), None) let sform_typecons ctx loc sargs ot = @@ -1411,7 +1434,7 @@ let sform_identifier ctx loc sargs ot = (if not (name = "") then let idx = match mv with | Metavar (idx, _, _) -> idx - | _ -> fatal loc "newMetavar returned a non-Metavar" in + | _ -> fatal ~loc "newMetavar returned a non-Metavar" in rmmap := SMap.add name idx (!rmmap)); (mkSusp mv subst, match ot with Some _ -> Checked | None -> Lazy) @@ -1592,7 +1615,8 @@ let sform_load usr_elctx loc sargs ot = read_file file_name usr_elctx else read_file file_name !sform_default_ectx - | _ -> (error loc "argument to load should be one file name (String)"; !sform_default_ectx) in + | _ -> (error ~loc "argument to load should be one file name (String)"; + !sform_default_ectx) in (* get lexp_context *) let usr_lctx = ectx_to_lctx usr_elctx in @@ -1679,8 +1703,8 @@ let default_ectx let idx = senv_lookup name elctx in let v = mkVar ((dloc, Some name), idx) in BI.set_predef name v) BI.predef_names; - with e -> - warning dloc "Predef not found"; in + with Senv_Lookup_Fail _ -> + warning "Predef not found"; in (* Empty context *) let lctx = empty_elab_context in @@ -1707,7 +1731,10 @@ let default_ectx (fun () -> read_file (btl_folder ^ "/pervasive.typer") lctx) in let _ = sform_default_ectx := ectx in ectx - with (Stop_Compilation _) -> fatal dloc "compilation stopped in default context" + with e -> + error "Compilation stopped in default context"; + Log.print_and_clear_log (); + raise e let default_rctx = EV.from_ectx default_ectx @@ -1723,7 +1750,7 @@ let lexp_expr_str str ctx = List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) lexps; lexps - with Stop_Compilation s -> (print_string s; []) + with Log.Stop_Compilation s -> [] let lexp_decl_str str ctx = try let tenv = default_stt in @@ -1731,7 +1758,7 @@ let lexp_decl_str str ctx = let limit = Some ";" in let sdecls = sexp_parse_str str tenv grm limit in lexp_p_decls sdecls ctx - with Stop_Compilation s -> (print_string s; ([],ctx)) + with Log.Stop_Compilation s -> ([],ctx) (* Eval String @@ -1742,7 +1769,7 @@ let eval_expr_str str lctx rctx = try let lxps = lexp_expr_str str lctx in let elxps = List.map OL.erase_type lxps in EV.eval_all elxps rctx false - with Stop_Compilation s -> (print_string s; []) + with Log.Stop_Compilation s -> [] let eval_decl_str str lctx rctx = let prev_lctx, prev_rctx = lctx, rctx in @@ -1750,5 +1777,5 @@ let eval_decl_str str lctx rctx = let lxps, lctx = lexp_decl_str str lctx in let elxps = (List.map OL.clean_decls lxps) in (EV.eval_decls_toplevel elxps rctx), lctx - with Stop_Compilation s -> (print_string s; prev_rctx, prev_lctx) + with Log.Stop_Compilation s -> (prev_rctx, prev_lctx) ===================================== src/env.ml ===================================== @@ -30,7 +30,6 @@ * * --------------------------------------------------------------------------- *) -open Util (* msg_error *) open Fmt (* make_title, table util *) open Sexp @@ -41,10 +40,10 @@ module L = Lexp module BI = Big_int module DB = Debruijn -let dloc = dummy_location +let dloc = Util.dummy_location -let error loc msg = msg_error "ENV" loc msg; raise (internal_error msg) -let warning loc msg = msg_warning "ENV" loc msg +let fatal = Log.log_fatal ~section:"ENV" +let warning = Log.log_warning ~section:"ENV" let str_idx idx = "[" ^ (string_of_int idx) ^ "]" @@ -81,11 +80,11 @@ let rec value_equal a b = | Vin (c1), Vin (c2) -> c1 = c2 | Vout (c1), Vout (c2) -> c2 = c2 | Vcommand (f1), Vcommand (f2) -> f1 = f2 - | Vundefined, _ | _, Vundefined -> warning dloc "Vundefined"; false - | Vtype e1, Vtype e2 -> warning dloc "Vtype"; false + | Vundefined, _ | _, Vundefined -> warning "Vundefined"; false + | Vtype e1, Vtype e2 -> warning "Vtype"; false | Closure (s1, b1, ctx1), Closure (s2, b2, ctx2) - -> warning dloc "Closure"; + -> warning "Closure"; if (s1 != s2) then false else true | Vcons ((_, ct1), a1), Vcons ((_, ct2), a2) @@ -178,14 +177,14 @@ let get_rte_variable (name: vname) (idx: int) if n1 = n2 then x else ( - error dloc + fatal ("Variable lookup failure. Expected: \"" ^ n2 ^ "[" ^ (string_of_int idx) ^ "]" ^ "\" got \"" ^ n1 ^ "\""))) | _ -> x) with Not_found -> let n = match name with (_, Some n) -> n | _ -> "" in - error dloc ("Variable lookup failure. Var: \"" ^ + fatal ("Variable lookup failure. Var: \"" ^ n ^ "\" idx: " ^ (str_idx idx)) let add_rte_variable (name:vname) (x: value_type) (ctx: runtime_env) @@ -199,7 +198,7 @@ let set_rte_variable idx name (v: value_type) (ctx : runtime_env) = (match (n, name) with | ((_, Some n1), (_, Some n2)) -> if (n1 != n2) then - error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) + fatal ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) | _ -> ()); ref_cell := v ===================================== src/eval.ml ===================================== @@ -82,13 +82,12 @@ let rec_depth trace = List.length b (* eval error are always fatal *) -let error loc msg = - msg_error "EVAL" loc msg; - flush stdout; - raise (internal_error msg) +let error loc ?print_action msg = + Log.log_error ~section:"EVAL" ~loc ?print_action msg; + Log.internal_error msg -let fatal = msg_fatal "EVAL" -let warning = msg_warning "EVAL" +let fatal loc msg = Log.log_fatal ~section:"EVAL" ~loc msg +let warning loc msg = Log.log_warning ~section:"EVAL" ~loc msg (* Print a message that look like this: * @@ -119,7 +118,7 @@ let debug_message error_type type_name type_string loc expr message = (* Print value name followed by the value in itself, finally throw an exception *) let value_fatal = debug_message fatal value_name value_string -let value_error = debug_message error value_name value_string +let value_error = debug_message (error ?print_action:None) value_name value_string let elexp_fatal = debug_message fatal elexp_name elexp_string @@ -341,16 +340,20 @@ let file_read loc depth args_val = match args_val with (* FIXME: Either rename it to "readline" and drop the second arg, * or actually pay attention to the second arg. *) | [Vin channel; Vint n] -> Vstring (input_line channel) - | _ -> List.iter (fun v -> value_print v; print_string "\n") args_val; - error loc "File.read expects an in_channel" + | _ -> error loc ~print_action:(fun _ -> + List.iter (fun v -> value_print v; print_newline ()) args_val; + ) + "File.read expects an in_channel. Actual arguments:" let file_write loc depth args_val = match args_val with | [Vout channel; Vstring msg] -> Vcommand (fun () -> fprintf channel "%s" msg; (* FIXME: This should be the unit value! *) Vundefined) - | _ -> List.iter (fun v -> value_print v) args_val; - error loc "File.write expects an out_channel and a string" + | _ -> error loc ~print_action:(fun _ -> + List.iter (fun v -> value_print v; print_newline ()) args_val; + ) + "File.write expects an out_channel and a string. Actual arguments:" let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) = @@ -470,9 +473,12 @@ and eval_call loc unef i f args = buildbody (arity - nargs - 1), buildctx args Myers.nil) - with Not_found - -> error loc ("Requested Built-in `" ^ name ^ "` does not exist") - | e -> error loc ("Exception thrown from primitive `" ^ name ^"`")) + with + | Not_found -> + error loc ("Requested Built-in `" ^ name ^ "` does not exist") + | e -> + warning loc ("Exception thrown from primitive `" ^ name ^"`"); + raise e) | Vtype e, _ (* We may call a Vlexp e.g. for "x = Map Int String". @@ -902,19 +908,27 @@ let array_empty loc depth args_val = match args_val with let test_fatal loc depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> Util.msg_user_fatal section loc msg) + Vcommand (fun () -> + Log.print_entry + (Log.mkEntry Log.Fatal ~kind:"(Unit test fatal)" ~loc ~section msg); + Log.user_error msg + ) | _ -> error loc "Test.fatal takes two String as argument" let test_warning loc depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> Util.msg_user_warning section loc msg; - tunit) + Vcommand (fun () -> + Log.print_entry + (Log.mkEntry Log.Warning ~kind:"(Unit test warning)" ~loc ~section msg); + tunit) | _ -> error loc "Test.warning takes two String as argument" let test_info loc depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> Util.msg_user_info section loc msg; - tunit) + Vcommand (fun () -> + Log.print_entry + (Log.mkEntry Log.Info ~kind:"(Unit test Info)" ~loc ~section msg); + tunit) | _ -> error loc "Test.info takes two String as argument" let test_location loc depth args_val = match args_val with @@ -1049,10 +1063,14 @@ let eval lxp ctx = eval lxp ctx ([], []) let debug_eval lxp ctx = try eval lxp ctx with e -> ( - print_rte_ctx (!global_eval_ctx); - print_eval_trace None; - raise e) - + let ectx = !global_eval_ctx in + let eval_trace = fst (get_trace ()) in + Log.log_info ~section:"EVAL" ~print_action:(fun _ -> + print_rte_ctx ectx; + print_eval_trace (Some eval_trace) + ) + "Exception occured during evaluation in the following context:"; + raise e) let eval_decls decls ctx = eval_decls decls ctx ([], []) ===================================== src/fmt.ml ===================================== @@ -156,3 +156,6 @@ let yellow = "\x1b[33m" let magenta = "\x1b[35m" let cyan = "\x1b[36m" let reset = "\x1b[0m" + +let color_string color str = + color ^ str ^ reset ===================================== src/inverse_subst.ml ===================================== @@ -169,11 +169,11 @@ let inverse (s: Lexp.subst) : Lexp.subst option = | Some s1 -> if is_identity (Lexp.scompose s s1) || is_identity (Lexp.scompose s1 s) then () - else (print_string ("Subst-inversion-bug: " - ^ subst_string s ^ " ∘ " - ^ subst_string s1 ^ " == " - ^ subst_string (Lexp.scompose s1 s) - ^ " !!\n")) + else (Log.log_debug ("Subst-inversion-bug: " + ^ subst_string s ^ " ∘ " + ^ subst_string s1 ^ " == " + ^ subst_string (Lexp.scompose s1 s) + ^ " !!\n")) | _ -> ()); res ===================================== src/lexer.ml ===================================== @@ -45,7 +45,7 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos (* The returned Sexp may not be a Node. *) : sexp * pretoken list * bytepos * charpos = match pts with - | [] -> (internal_error "No next token!") + | [] -> (Log.internal_error "No next token!") | (Preblock (sl, bpts, el) :: pts) -> (Block (sl, bpts, el), pts, 0, 0) | (Prestring (loc, str) :: pts) -> (String (loc, str), pts, 0, 0) | (Pretoken ({file;line;column;docstr}, name) :: pts') ===================================== src/lexp.ml ===================================== @@ -69,7 +69,7 @@ type ltype = lexp | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of U.location * (vname * lexp * ltype) list * lexp - | Arrow of arg_kind * vname * ltype * U.location * lexp + | Arrow of arg_kind * vname * ltype * U.location * ltype | Lambda of arg_kind * vname * ltype * lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) | Inductive of U.location * label @@ -166,7 +166,7 @@ let metavar_table = ref (U.IMap.empty : meta_subst) let metavar_lookup (id : meta_id) : metavar_info = try U.IMap.find id (!metavar_table) with Not_found - -> U.msg_fatal "LEXP" U.dummy_location "metavar lookup failure!" + -> Log.log_fatal ~section:"LEXP" "metavar lookup failure!" (********************** Hash-consing **********************) @@ -207,18 +207,18 @@ let mkCall (f, es) let mkSLlub' (e1, e2) = match (e1, e2) with | (SortLevel SLz, _) | (_, SortLevel SLz) - -> U.msg_fatal "internal" U.dummy_location "lub of SLz" + -> Log.log_fatal ~section:"internal" "lub of SLz" | (SortLevel (SLsucc _), SortLevel (SLsucc _)) - -> U.msg_fatal "internal" U.dummy_location "lub of two SLsucc" + -> Log.log_fatal ~section:"internal" "lub of two SLsucc" | ((SortLevel _ | Var _ | Metavar _ | Susp _), (SortLevel _ | Var _ | Metavar _ | Susp _)) -> SLlub (e1, e2) - | _ -> U.msg_fatal "internal" U.dummy_location "SLlub of non-level" + | _ -> Log.log_fatal ~section:"internal" "SLlub of non-level" let mkSLsucc e = match e with | SortLevel _ | Var _ | Metavar _ | Susp _ -> SLsucc e - | _ -> U.msg_fatal "internal" U.dummy_location "SLsucc of non-level" + | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level" (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. @@ -657,20 +657,29 @@ let debug_ppctx = ref ( ("print_implicit", Bool (true)); ("separate_decl" , Bool (false) );]) -let pp_pretty ctx = match SMap.find "pretty" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_type ctx = match SMap.find "print_type" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_dbi ctx = match SMap.find "print_dbi" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_size ctx = match SMap.find "indent_size" ctx with Int i -> i | _ -> U.typer_unreachable "" -let pp_color ctx = match SMap.find "color" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_decl ctx = match SMap.find "separate_decl" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_indent ctx = match SMap.find "indent_level" ctx with Int i -> i | _ -> U.typer_unreachable "" -let pp_parent ctx = match SMap.find "parent" ctx with Expr e -> e | _ -> U.typer_unreachable "" -let pp_meta ctx = match SMap.find "metavar" ctx with Expr e -> e | _ -> U.typer_unreachable "" -let pp_grammar ctx = match SMap.find "grammar" ctx with Predtl p -> p | _ -> U.typer_unreachable "" -let pp_colsize ctx = match SMap.find "col_size" ctx with Int i -> i | _ -> U.typer_unreachable "" -let pp_colmax ctx = match SMap.find "col_max" ctx with Int i -> i | _ -> U.typer_unreachable "" -let pp_erasable ctx = match SMap.find "print_erasable" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_implicit ctx = match SMap.find "print_implicit" ctx with Bool b -> b | _ -> U.typer_unreachable "" +let smap_bool s ctx = + match SMap.find s ctx with Bool b -> b | _ -> failwith "Unreachable" +and smap_int s ctx = + match SMap.find s ctx with Int i -> i | _ -> failwith "Unreachable" +and smap_lexp s ctx = + match SMap.find s ctx with Expr e -> e | _ -> failwith "Unreachable" +and smap_predtl s ctx = + match SMap.find s ctx with Predtl tl -> tl | _ -> failwith "Unreachable" + +let pp_pretty = smap_bool "pretty" +let pp_type = smap_bool "print_type" +let pp_dbi = smap_bool "print_dbi" +let pp_size = smap_int "indent_size" +let pp_color = smap_bool "color" +let pp_decl = smap_bool "separate_decl" +let pp_indent = smap_int "indent_level" +let pp_parent = smap_lexp "parent" +let pp_meta = smap_lexp "metavar" +let pp_grammar = smap_predtl "grammar" +let pp_colsize = smap_int "col_size" +let pp_colmax = smap_int "col_max" +let pp_erasable = smap_bool "print_erasable" +let pp_implicit = smap_bool "print_implicit" let set_col_size p ctx = SMap.add "col_size" (Int p) ctx let add_col_size p ctx = set_col_size ((pp_colsize ctx) + p) ctx ===================================== src/list.ml ===================================== @@ -0,0 +1,29 @@ +(* list.ml --- + * + * Copyright (C) 2019 Free Software Foundation, Inc. + * + * Author: Simon Génier <simon.genier(a)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 ===================================== @@ -0,0 +1,217 @@ +(* log.ml --- User Errors/Warnings log for Typer. -*- coding: utf-8 -*- + +Copyright (C) 2019 Free Software Foundation, Inc. + +Author: Jean-Alexandre Barszcz <jalex_b(a)hotmail.com> +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 Util + +(* LOGGING LEVELS *) + +type log_level = Nothing | Fatal | Error | Warning | Info | Debug + +let int_of_level lvl = + match lvl with + | Nothing -> -1 (* We might not want to print anything during testing *) + | Fatal -> 0 | Error -> 1 | Warning -> 2 | Info -> 3 | Debug -> 4 + +let level_of_int i = + match i with + | _ when i < 0 -> Nothing + | 0 -> Fatal | 1 -> Error | 2 -> Warning | 3 -> Info + | _ -> Debug + +let string_of_level lvl = + match lvl with + | Nothing -> "Nothing" + | Fatal -> "Fatal" + | Error -> "Error" + | Warning -> "Warning" + | Info -> "Info" + | Debug -> "Debug" + +let level_of_string str = + match Util.string_uppercase str with + | "NOTHING" -> Nothing + | "FATAL" -> Fatal + | "ERROR" -> Error + | "WARNING" -> Warning + | "INFO" -> Info + | "DEBUG" -> Debug + | _ -> invalid_arg ("`"^str^"` is not a logging level") + +let level_color lvl = + match lvl with + | Nothing -> None + | Fatal -> Some Fmt.red + | Error -> Some Fmt.red + | Warning -> Some Fmt.yellow + | Info -> Some Fmt.cyan + | Debug -> Some Fmt.magenta + +(* LOGGING CONFIGURATION *) + +type log_config = { + mutable level : log_level; + mutable print_at_log : bool; + mutable print_in_reverse : bool; + mutable color : bool; + } + +let typer_log_config = { + level = Warning; + print_at_log = false; + print_in_reverse = false; + color = true; + } + +(* LOG DEFINITION *) + +type log_entry = { + level : log_level; + kind : string option; + section : string option; + print_action : (unit -> unit) option; + loc : location option; + msg : string; + } + +type log = log_entry list + +let empty_log = [] + +let typer_log = ref empty_log + +(* PRIVATE OPERATIONS *) + +let mkEntry level ?kind ?section ?print_action ?loc msg = + {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 + | None -> 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 + 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 = + print_endline (string_of_log_entry entry); + match entry.print_action with + | Some f -> f () + | None -> () + +let log_entry (entry : log_entry) = + if (entry.level <= typer_log_config.level) + then ( + log_push entry; + if (typer_log_config.print_at_log) + then + (print_entry entry; + flush stdout) + ) + +let count_msgs (lvlp : log_level -> bool) = + let count_step count {level} = + if lvlp level then count + 1 else count + in + List.fold_left count_step 0 !typer_log + +let error_count () = count_msgs (fun level -> level <= Error) +let warning_count () = count_msgs (fun level -> level = Warning) + +(* PUBLIC INTERFACE *) + +let set_typer_log_level lvl = + typer_log_config.level <- lvl + +let set_typer_log_level_str str = + try set_typer_log_level (level_of_int (int_of_string str)) + with + _ -> set_typer_log_level (level_of_string str) + +let increment_log_level () = + typer_log_config.level + |> int_of_level + |> (+) 1 + |> level_of_int + |> set_typer_log_level + +let clear_log () = typer_log := empty_log + +let print_log () = + let reverse = typer_log_config.print_in_reverse in + let l = if reverse then !typer_log else List.rev !typer_log in + List.iter print_entry l + +let print_and_clear_log () = + print_log (); clear_log () + +let log_msg level ?kind ?section ?print_action ?loc msg = + log_entry (mkEntry level ?kind ?section ?print_action ?loc msg) + +exception Internal_error of string +let internal_error s = raise (Internal_error s) + +exception User_error of string +let user_error s = raise (User_error s) + +exception Stop_Compilation of string +let stop_compilation s = raise (Stop_Compilation s) + +let log_fatal ?section ?print_action ?loc m = + log_msg Fatal ~kind:"[X] Fatal " ?section ?print_action ?loc m; + internal_error "Compiler Fatal Error" +let log_error = log_msg Error ?kind:None +let log_warning = log_msg Warning ?kind:None +let log_info = log_msg Info ?kind:None +let log_debug = log_msg Debug ?kind:None + +let stop_on_error () = + let count = error_count () in + if (0 < count) then + stop_compilation + ("Compiler stopped after: "^(string_of_int count)^" errors\n") + +let stop_on_warning () = + stop_on_error (); + let count = warning_count () in + if (0 < count) then + stop_compilation + ("Compiler stopped after: "^(string_of_int count)^" warnings\n") + +(* Compiler Internal Debug print *) +let debug_msg expr = + if Debug <= typer_log_config.level then (print_string expr; flush stdout) + +let not_implemented_error () = internal_error "not implemented" ===================================== src/opslexp.ml ===================================== @@ -38,6 +38,9 @@ module S = Subst (* module L = List *) module DB = Debruijn +let error_tc = Log.log_error ~section:"TC" +let warning_tc = Log.log_warning ~section:"TC" + (* `conv_erase` is supposed to be safe according to the ICC papers. *) let conv_erase = true (* Makes conv ignore erased terms. *) @@ -161,7 +164,7 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = -> match default with | Some (v,default) -> lexp_whnf (push_susp default (S.substitute e')) ctx - | _ -> U.msg_error "WHNF" l + | _ -> Log.log_error ~section:"WHNF" ~loc:l ("Unhandled constructor " ^ name ^ "in case expression"); mkCase (l, e, rt, branches, default) in @@ -399,17 +402,17 @@ let rec check'' erased ctx e = let check = check'' in let assert_type ctx e t t' = if conv_p ctx t t' then () - else (U.msg_error "TC" (lexp_location e) + else (error_tc ~loc:(lexp_location e) ("Type mismatch for " ^ lexp_string (L.clean e) ^ " : " ^ lexp_string (L.clean t) ^ " != " ^ lexp_string (L.clean t')); - (* U.internal_error "Type mismatch" *)) in + (* Log.internal_error "Type mismatch" *)) in let check_type erased ctx t = let s = check erased ctx t in (match lexp_whnf s ctx with | Sort _ -> () - | _ -> U.msg_error "TC" (lexp_location t) + | _ -> error_tc ~loc:(lexp_location t) ("Not a proper type: " ^ lexp_string t)); (* FIXME: return the `sort` rather than the surrounding `lexp`! *) s in @@ -419,7 +422,7 @@ let rec check'' erased ctx e = | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) - -> (U.msg_error "TC" (lexp_location e) "Unsupported immediate value!"; + -> (error_tc ~loc:(lexp_location e) "Unsupported immediate value!"; DB.type_int) | SortLevel SLz -> DB.type_level | SortLevel (SLsucc e) @@ -440,8 +443,8 @@ let rec check'' erased ctx e = mkSort (l, Stype (mkSortLevel (SLsucc e))) | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) - -> ((* U.msg_error "TC" (lexp_location e) "Reached unreachable sort!"; - * U.internal_error "Reached unreachable sort!"; *) + -> ((* error_tc ~loc:(lexp_location e) "Reached unreachable sort!"; + * Log.internal_error "Reached unreachable sort!"; *) DB.sort_omega) | Builtin (_, t, _) -> let _ = check_type DB.set_empty Myers.nil t in @@ -450,7 +453,7 @@ let rec check'' erased ctx e = (* FIXME: Check recursive references. *) | Var (((l, name), idx) as v) -> if DB.set_mem idx erased then - U.msg_error "TC" l + error_tc ~loc:l ("Var `" ^ maybename name ^ "`" ^ " can't be used here, because it's `erasable`"); lookup_type ctx v @@ -483,14 +486,14 @@ let rec check'' erased ctx e = match sort_compose ctx l ak k1 k2 with | SortResult k -> k | SortInvalid - -> U.msg_error "TC" l "Invalid arrow: inner TypelLevel argument"; + -> error_tc ~loc:l "Invalid arrow: inner TypelLevel argument"; mkSort (l, StypeOmega) | SortK1NotType - -> (U.msg_error "TC" (lexp_location t1) + -> (error_tc ~loc:(lexp_location t1) "Not a proper type"; mkSort (l, StypeOmega)) | SortK2NotType - -> (U.msg_error "TC" (lexp_location t2) + -> (error_tc ~loc:(lexp_location t2) "Not a proper type"; mkSort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) @@ -508,12 +511,12 @@ let rec check'' erased ctx e = match lexp_whnf ft ctx with | Arrow (ak', v, t1, l, t2) -> if not (ak == ak') then - (U.msg_error "TC" (lexp_location arg) + (error_tc ~loc:(lexp_location arg) "arg kind mismatch"; ()) else (); assert_type ctx arg t1 at; mkSusp t2 (S.substitute arg) - | _ -> (U.msg_error "TC" (lexp_location arg) + | _ -> (error_tc ~loc:(lexp_location arg) ("Calling a non function (type = " ^ lexp_string ft ^ ")!"); ft)) @@ -538,14 +541,15 @@ let rec check'' erased ctx e = (* We need to unshift because the final type * cannot refer to the fields! *) (mkSusp level' (L.sunshift n)) - | tt -> U.msg_error "TC" (lexp_location t) - ("Field type " - ^ lexp_string t - ^ " is not a Type! (" - ^ lexp_string tt ^")"); - DB.print_lexp_ctx ictx; - (* U.internal_error "Oops"; *) - level), + | tt -> error_tc ~loc:(lexp_location t) + ~print_action:(fun _ -> + DB.print_lexp_ctx ictx; print_newline () + ) + ("Field type " + ^ lexp_string t + ^ " is not a Type! (" + ^ lexp_string tt ^")"); + level), DB.lctx_extend ictx v Variable t, DB.set_sink 1 erased, n + 1)) @@ -578,7 +582,7 @@ let rec check'' erased ctx e = (* We don't check aarg's type, because we assume that `check` * returns a valid type. *) -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (U.msg_error "TC" l + | _,_ -> (error_tc ~loc:l "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in SMap.iter @@ -595,7 +599,7 @@ let rec check'' erased ctx e = (S.cons (Var (vdef, 0)) (S.mkShift s 1)) vdefs fieldtypes - | _,_ -> (U.msg_error "TC" l + | _,_ -> (error_tc ~loc:l "Wrong number of args to constructor!"; (erased, ctx)) in let (nerased, nctx) = mkctx erased ctx s vdefs fieldtypes in @@ -607,15 +611,15 @@ let rec check'' erased ctx e = (match default with | Some (v, d) -> if diff <= 0 then - U.msg_warning "TC" l "Redundant default clause"; + warning_tc ~loc:l "Redundant default clause"; let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in assert_type nctx d (mkSusp ret (S.shift 1)) (check (DB.set_sink 1 erased) nctx d) | None -> if diff > 0 then - U.msg_error "TC" l ("Non-exhaustive match: " + error_tc ~loc:l ("Non-exhaustive match: " ^ string_of_int diff ^ " cases missing")) - | _,_ -> U.msg_error "TC" l "Case on a non-inductive type!"); + | _,_ -> error_tc ~loc:l "Case on a non-inductive type!"); ret | Cons (t, (l, name)) -> (match lexp_whnf t ctx with @@ -643,10 +647,10 @@ let rec check'' erased ctx e = buildtype fargs) in buildtype fargs with Not_found - -> (U.msg_error "TC" l + -> (error_tc ~loc:l ("Constructor \"" ^ name ^ "\" does not exist"); DB.type_int)) - | _ -> (U.msg_error "TC" (lexp_location e) + | _ -> (error_tc ~loc:(lexp_location e) ("Cons of a non-inductive type: " ^ lexp_string t); DB.type_int)) @@ -658,7 +662,7 @@ let rec check'' erased ctx e = let check' ctx e = let res = check'' DB.set_empty ctx e in - (U.stop_on_error (); res) + (Log.stop_on_error (); res) let check = check' @@ -917,7 +921,7 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Sort _ -> E.Type lxp (* Still useful to some extent. *) | L.Inductive(l, label, _, _) -> E.Type lxp - | L.Metavar _ -> U.internal_error "Metavar in erase_type" + | L.Metavar _ -> Log.internal_error "Metavar in erase_type" and filter_arg_list lst = let rec filter_arg_list lst acc = @@ -955,7 +959,7 @@ and clean_map cases = (** Turning a set of declarations into an object. **) let ctx2tup ctx nctx = - (*U.debug_msg ("Entering ctx2tup\n");*) + (*Log.debug_msg ("Entering ctx2tup\n");*) assert (M.length nctx >= M.length ctx && ctx == M.nthcdr (M.length nctx - M.length ctx) nctx); let rec get_blocs nctx blocs = @@ -973,7 +977,7 @@ let ctx2tup ctx nctx = let type_label = (loc, "record") in let offset = List.length types in let types = List.rev types in - (*U.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*) + (*Log.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*) Call (Cons (Inductive (loc, type_label, [], SMap.add cons_name (List.map (fun (oname, t) ===================================== src/option.ml ===================================== @@ -0,0 +1,47 @@ +(* option.ml --- + * + * Copyright (C) 2019 Free Software Foundation, Inc. + * + * Author: Simon Génier <simon.genier(a)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/pexp.ml ===================================== @@ -25,7 +25,7 @@ open Sexp (* Symbol *) open Lexer open Grammar -let pexp_error = msg_error "PEXP" +let pexp_error loc = Log.log_error ~section:"PEXP" ~loc (*************** The Pexp Parser *********************) ===================================== src/positivity.ml ===================================== @@ -0,0 +1,97 @@ +(* positivity.ml --- + * + * Copyright (C) 2019 Free Software Foundation, Inc. + * + * Author: Simon Génier <simon.genier(a)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/prelexer.ml ===================================== @@ -22,7 +22,7 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) open Util -let prelexer_error = msg_error "PRELEXER" +let prelexer_error loc = Log.log_error ~section:"PRELEXER" ~loc type pretoken = | Pretoken of location * string ===================================== src/sexp.ml ===================================== @@ -24,7 +24,8 @@ open Util open Prelexer open Grammar -let sexp_error = msg_error "SEXP" +let sexp_error ?print_action loc msg = + Log.log_error ~section:"SEXP" ?print_action ~loc msg type integer = (* Num.num *) int type symbol = location * string @@ -119,7 +120,7 @@ let rec sexp_parse (g : grammar) (rest : sexp list) let sexp_parse = sexp_parse g in let rec compose_symbol (ss : symbol list) = match ss with - | [] -> (internal_error "empty operator!") + | [] -> (Log.internal_error "empty operator!") | (l,_)::_ -> (l, String.concat "_" (List.map (fun (_,s) -> s) (List.rev ss))) in @@ -201,19 +202,19 @@ let sexp_parse_all grm tokens limit : sexp * token list = | Some token -> match SMap.find token grm with | (Some ll, Some _) -> ll + 1 - | _ -> (internal_error ("Can't find level of \""^token^"\"")) + | _ -> (Log.internal_error ("Can't find level of \""^token^"\"")) in let (e, rest) = sexp_parse grm tokens level [] [] [] in let se = match e with | Node (Symbol (_, ""), [e]) -> e | Node (Symbol (_, ""), e::es) -> Node (e, es) - | _ -> (internal_error "Didn't find a toplevel") in + | _ -> (Log.internal_error "Didn't find a toplevel") in match rest with | [] -> (se,rest) | Symbol (l,t) :: rest -> if not (Some t = limit) then sexp_error l ("Stray closing token: \"" ^ t ^ "\""); (se,rest) - | _ -> (internal_error "Stopped parsing before the end!") + | _ -> (Log.internal_error "Stopped parsing before the end!") (* "sexp_p" is for "parsing" and "sexp_u" is for "unparsing". *) ===================================== src/unification.ml ===================================== @@ -27,6 +27,8 @@ module DB = Debruijn (** Provide unify function for unifying two Lambda-Expression *) +let log_info = Log.log_info ~section:"UNIF" + (* :-( *) let global_last_metavar = ref (-1) (*The first metavar is 0*) @@ -45,7 +47,7 @@ let associate (id: meta_id) (lxp: lexp) (subst: meta_subst) : meta_subst = U.IMap.add id (MVal lxp) subst let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with - | MVal _ -> U.internal_error + | MVal _ -> Log.internal_error "Checking occurrence of an instantiated metavar!!" | MVar (sl, _, _) -> let rec oi e = match e with @@ -57,7 +59,7 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | Sort (_, (StypeOmega | StypeLevel)) -> false | Builtin _ -> false | Var (_, i) -> false - | Susp (e, s) -> U.internal_error "`e` should be \"clean\" here!?" + | Susp (e, s) -> Log.internal_error "`e` should be \"clean\" here!?" (* ; oi (push_susp e s) *) | Let (_, defs, e) -> List.fold_left (fun o (_, e, t) -> o || oi e || oi t) (oi e) defs @@ -81,7 +83,7 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | Metavar (id', _, name) when id' = id -> true | Metavar (id', _, _) -> (match metavar_lookup id' with - | MVal e -> U.internal_error "`e` should be \"clean\" here!?" + | MVal e -> Log.internal_error "`e` should be \"clean\" here!?" (* ; oi e *) | MVar (sl', t, cl) -> if sl' > sl then @@ -227,17 +229,16 @@ and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) : return_type = let unif idx s lxp = let t = match metavar_lookup idx with - | MVal _ -> U.internal_error + | MVal _ -> Log.internal_error "`lexp_whnf` returned an instantiated metavar!!" | MVar (_, t, _) -> push_susp t s in match Inverse_subst.apply_inv_subst lxp s with | exception Inverse_subst.Not_invertible - -> print_string "Unification of metavar failed:\n "; - print_string ("?[" ^ subst_string s ^ "]"); - print_string "\nAgainst:\n "; - lexp_print lxp; - print_string "\n"; - None + -> log_info ?loc:None ("Unification of metavar failed:\n " + ^ "?[" ^ subst_string s ^ "]" + ^ "\nAgainst:\n " + ^ lexp_string lxp ^ "\n"); + None | lxp' when occurs_in idx lxp' -> None | lxp' -> metavar_table := associate idx lxp' (!metavar_table); @@ -245,11 +246,12 @@ and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) | Some [] as r -> r (* FIXME: Let's ignore the error for now. *) | _ - -> print_string ("Unification of metavar type failed:\n " - ^ lexp_string (Lexp.clean t) ^ " != " - ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) - ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); - Some [] in + -> log_info ?loc:None + ("Unification of metavar type failed:\n " + ^ lexp_string (Lexp.clean t) ^ " != " + ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) + ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); + Some [] in match lxp2 with | Metavar (idx2, s2, _) -> if idx = idx2 then ===================================== src/util.ml ===================================== @@ -51,114 +51,6 @@ let loc_string loc = let loc_print loc = print_string (loc_string loc) -(* - * -1 - Nothing (* During testing we may want to produce errors *) - * 0 - Fatal - * 1 - Error - * 2 - Warning - * 3 - Info - *) - -let typer_verbose = ref 20 - -exception Internal_error of string -let internal_error s = raise (Internal_error s) - -exception Unreachable_error of string -let typer_unreachable s = raise (Unreachable_error s) - -exception User_error of string -let user_error s = raise (User_error s) - -exception Stop_Compilation of string -let stop_compilation s = raise (Stop_Compilation s) - -(* `error list * warning list` both of type `level * kind * section * loc * msg` *) -type error_log_type = ((int * string * string * location * string) list * - (int * string * string * location * string) list) - -let empty_error_log : error_log_type = ([],[]) - -let error_log = ref empty_error_log - -let error_count () : int = let errors, _ = !error_log in - List.length errors - -let warning_count () : int = let _, warnings = !error_log in - List.length warnings - -let new_error lvl kind section loc msg = let errors, warnings = !error_log in - error_log := ((lvl,kind,section,loc,msg)::errors,warnings) - -let new_warning lvl kind section loc msg = let errors, warnings = !error_log in - error_log := (errors,(lvl,kind,section,loc,msg)::warnings) - -let reset_error_log () = error_log := empty_error_log - -(* Section is the name of the compilation step [for debugging] *) -(* 'prerr' output is ugly *) -let msg_message (error : bool) lvl kind section (loc: location) msg = - let message = (loc.file - ^ ":" ^ string_of_int loc.line - ^ ":" ^ string_of_int loc.column - ^ ":" ^ kind - ^ (if section = "" then " " else "(" ^ section ^ ") ") - ^ msg ^ "\n") in - - if error then - new_error lvl kind section loc msg - else - new_warning lvl kind section loc msg; - - if lvl <= !typer_verbose then - print_string message - else () - -let stop_on_error () = if (0 < (error_count ())) then - (let count = error_count () in - reset_error_log (); - stop_compilation - ("Compiler stopped after: "^(string_of_int count)^" error\n")) - else () - -let stop_on_warning () = (stop_on_error (); - if (0 < (warning_count ())) then - let count = warning_count () in - reset_error_log (); - stop_compilation - ("Compiler stopped after: "^(string_of_int count)^" warning\n") - else ()) - -let catch_error () = try stop_on_error () - with e -> match e with - | Stop_Compilation msg -> print_string msg - | _ -> () - -let msg_fatal s l m = - msg_message false 0 "[X] Fatal " s l m; - flush stdout; - reset_error_log (); - internal_error "Compiler Fatal Error" - -let msg_error = msg_message true 1 "Error:" -let msg_warning = msg_message false 2 "Warning:" -let msg_info = msg_message false 3 "Info:" - -let msg_user_fatal s l m = - msg_message true 1 "(Unit test fatal):" s l m; - flush stdout; - reset_error_log (); - user_error "User Fatal Error" - -let msg_user_warning = msg_message false 2 "(Unit test warning):" -let msg_user_info = msg_message false 3 "(Unit test info):" - -(* Compiler Internal Debug print *) -let debug_msg expr = - if 4 <= !typer_verbose then (print_string expr; flush stdout) else () - -let not_implemented_error () = internal_error "not implemented" - let string_implode chars = String.concat "" (List.map (String.make 1) chars) let string_sub str b e = String.sub str b (e - b) @@ -166,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 ===================================== tests/positivity_test.ml ===================================== @@ -0,0 +1,70 @@ +(* positivity_test.ml --- + * + * Copyright (C) 2019 Free Software Foundation, Inc. + * + * Author: Simon Génier <simon.genier(a)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(a)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 ===================================== tests/utest_lib.ml ===================================== @@ -76,7 +76,7 @@ let global_ftitle = ref "" let set_verbose lvl = global_verbose_lvl := lvl; - (if lvl >= 3 then U.typer_verbose := 20 else U.typer_verbose := (-1)) + Log.set_typer_log_level (if lvl >= 3 then Log.Debug else Log.Nothing) let arg_defs = [ ("--verbose=", View it on GitLab: https://gitlab.com/monnier/typer/compare/a8096766de90c63606e27d8b3a75db1d19… -- View it on GitLab: https://gitlab.com/monnier/typer/compare/a8096766de90c63606e27d8b3a75db1d19… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] 9 commits: Extract logging from util.ml
by Jean-Alexandre Barszcz 10 Oct '19

10 Oct '19

Jean-Alexandre Barszcz pushed to branch master at Stefan / Typer Commits: 9455fa18 by Jean-Alexandre Barszcz at 2019-10-04T01:46:06Z Extract logging from util.ml - - - - - c1458d9a by Jean-Alexandre Barszcz at 2019-10-04T01:46:06Z Replace typer_unreachable exception with 'failwith' - - - - - 82fa3593 by Jean-Alexandre Barszcz at 2019-10-04T01:46:06Z Refactor logging - - - - - 51251f1f by Jean-Alexandre Barszcz at 2019-10-04T01:46:06Z Add optional color to logging - - - - - 2a2afc56 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Print errors/warnings all at once, after compilation stops - - - - - 09952ed7 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Print the log in default context - - - - - c02e28bc by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Add an option to control the verbosity/logging level - - - - - f41b8bb3 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Always print the log after evaluation If there are warnings (or other messages of lesser priority in the log), we want to print them. Similarly, errors for which we were able to recover might still exist in the log. Regardless of whether compilation has been stopped, we thus print the log. - - - - - b948d4c9 by Jean-Alexandre Barszcz at 2019-10-10T06:52:31Z Print test messages instead of logging them - - - - - 18 changed files: - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml - + src/log.ml - src/opslexp.ml - src/pexp.ml - src/prelexer.ml - src/sexp.ml - src/unification.ml - src/util.ml - tests/utest_lib.ml Changes: ===================================== src/REPL.ml ===================================== @@ -63,8 +63,16 @@ let print_input_line i = ralign_print_int i 2; print_string "] >> " -let ieval_error loc msg = - msg_error "IEVAL" loc msg +let ieval_error = Log.log_error ~section:"IEVAL" + +let print_and_clear_log () = + if (not Log.typer_log_config.print_at_log) then + Log.print_and_clear_log () + +let handle_stopped_compilation msg = + print_and_clear_log (); + print_string msg; print_newline (); + flush stdout (* Read stdin for input. Returns only when the last char is ';' * We can use '%' to prevent parsing @@ -207,7 +215,7 @@ let readfiles files (i, lctx, rctx) prt = (List.iter (print_eval_result i) ret; (i + 1, lctx, rctx)) with Sys_error _ -> ( - ieval_error dloc ("file \"" ^ file ^ "\" does not exist."); + ieval_error ("file \"" ^ file ^ "\" does not exist."); (i, lctx, rctx)) ) (i, lctx, rctx) files @@ -231,8 +239,8 @@ let rec repl i clxp rctx = let (i, clxp, rctx) = try readfiles args (i, clxp, rctx) false - with Stop_Compilation s -> - (print_string s; (i,clxp,rctx)) + with Log.Stop_Compilation msg -> + (handle_stopped_compilation msg; (i,clxp,rctx)) in repl clxp rctx; | "%who"::args | "%w"::args -> ( @@ -247,18 +255,25 @@ let rec repl i clxp rctx = repl clxp rctx) | cmd::_ -> - ieval_error dloc (" \"" ^ cmd ^ "\" is not a correct repl command"); + ieval_error (" \"" ^ cmd ^ "\" is not a correct repl command"); repl clxp rctx | _ -> repl clxp rctx) (* eval input *) - | _ -> ( + | _ -> try let (ret, clxp, rctx) = (ieval_string ipt clxp rctx) in + print_and_clear_log (); List.iter (print_eval_result i) ret; repl clxp rctx - with e -> match e with - | Stop_Compilation msg -> (print_string msg; repl clxp rctx) - | _ -> catch_error (); repl clxp rctx) + with + | Log.Stop_Compilation msg -> + (handle_stopped_compilation msg; repl clxp rctx) + | Log.Internal_error msg -> + (handle_stopped_compilation ("Internal error: " ^ msg); + repl clxp rctx) + | Log.User_error msg -> + (handle_stopped_compilation ("Fatal user error: " ^ msg); + repl clxp rctx) let arg_files = ref [] @@ -266,6 +281,9 @@ let arg_files = ref [] (* ./typer [options] files *) let arg_defs = [ ("--batch", Arg.Set arg_batch, "Don't run the interactive loop"); + ("--verbosity", + Arg.String Log.set_typer_log_level_str, "Set the logging level"); + ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity"); (* ("--debug", Arg.Set arg_debug, "Print the Elexp representation") *) (*"-I", Arg.String (fun f -> searchpath := f::!searchpath), @@ -287,8 +305,19 @@ let main () = print_string (make_sep '-'); flush stdout); - let (i, ectx, rctx) = readfiles (List.rev !arg_files) (1, ectx, rctx) - (not !arg_batch) in + let (i, ectx, rctx) = ( + try + let res = + readfiles (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch) in + print_and_clear_log (); res + with + | Log.Stop_Compilation msg -> + handle_stopped_compilation msg; exit 1 + | Log.Internal_error msg -> + handle_stopped_compilation ("Internal error: " ^ msg); exit 1 + | Log.User_error msg -> + handle_stopped_compilation ("Fatal user error: " ^ msg); exit 1 + ) in flush stdout; ===================================== src/builtin.ml ===================================== @@ -64,8 +64,9 @@ open Lexp module DB = Debruijn module E = Env -let error loc msg = msg_error "BUILT-IN" loc msg; raise (internal_error msg) -let warning loc msg = msg_warning "BUILT-IN" loc msg +let log_raise_error ?loc msg = + Log.log_error ~section:"BUILT-IN" ?loc msg; + Log.internal_error msg let predef_names = [ "cons"; (* FIXME: Should be used but isn't! *) @@ -87,7 +88,7 @@ let get_predef (name: string) (ctx: DB.elab_context) : lexp = try let r = (DB.get_size ctx) - !builtin_size - 0 in let p = SMap.find name (!predef_map) in mkSusp p (S.shift r) - with Not_found -> error dummy_location ("\""^ name ^ "\" was not predefined") + with Not_found -> log_raise_error ("\""^ name ^ "\" was not predefined") let set_predef name lexp = predef_map := SMap.add name lexp (!predef_map) @@ -131,9 +132,9 @@ let v2o_list v = match v with | E.Vcons ((_, "cons"), [hd; tl]) -> v2o_list (hd::acc) tl | E.Vcons ((_, "nil"), []) -> List.rev acc - | _ -> print_string (E.value_name v); print_string "\n"; - E.value_print v; - error dloc "List conversion failure'" in + | _ -> log_raise_error ~loc:(E.value_location v) ( + "Failed to convert the " ^ E.value_name v ^ " with value :\n" + ^ E.value_string v ^ "\n to a list.") in v2o_list [] v (* Map of lexp builtin elements accessible via (## <name>). *) ===================================== src/debruijn.ml ===================================== @@ -42,8 +42,7 @@ open Fmt module S = Subst -let error l m = msg_error "DEBRUIJN" l m; internal_error m -let warning = msg_warning "DEBRUIJN" +let fatal = Log.log_fatal ~section:"DEBRUIJN" (* Handling scoping/bindings is always tricky. So it's always important * to keep in mind for *every* expression which is its context. @@ -316,17 +315,17 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = | (((_, Some name), _, _), Some ename) -> (* Check if names match *) if not (ename = name) then - (print_lexp_ctx ctx; - error loc ("DeBruijn index " - ^ string_of_int dbi - ^ " refers to wrong name. " - ^ "Expected: `" ^ ename - ^ "` got `" ^ name ^ "`")) + fatal ~loc ~print_action:(fun _ -> + print_lexp_ctx ctx; print_newline ()) + ("DeBruijn index " ^ string_of_int dbi + ^ " refers to wrong name. " + ^ "Expected: `" ^ ename + ^ "` got `" ^ name ^ "`") | _ -> () in ret) with - Not_found -> error loc ("DeBruijn index " + Not_found -> fatal ~loc ("DeBruijn index " ^ string_of_int dbi ^ " of `" ^ maybename oename ^ "` out of bounds!") @@ -366,7 +365,7 @@ let rec lctx_view lctx = | _ -> CVfix (defs, lctx) in loop 2 lctx [(loname, def, t)] | Myers.Mcons ((_, LetDef (o, def), _), _, _, _) when o > 1 - -> U.internal_error "Unexpected lexp_context shape!" + -> fatal "Unexpected lexp_context shape!" | Myers.Mcons ((loname, odef, t), lctx, _, _) -> CVlet (loname, odef, t, lctx) ===================================== src/elab.ml ===================================== @@ -69,21 +69,28 @@ let btl_folder = try Sys.getenv "TYPER_BUILTINS" with Not_found -> "./btl" -let warning = msg_warning "ELAB" -let error = msg_error "ELAB" -let fatal = msg_fatal "ELAB" - -(* Print Lexp name followed by the lexp in itself, finally throw an exception *) -let debug_message error_type type_name type_string loc expr message = - EV.debug_messages error_type loc - message [ - (type_name expr) ^ ": " ^ (type_string expr); - ] - -let lexp_fatal = debug_message fatal lexp_name lexp_string -let lexp_warning = debug_message warning lexp_name lexp_string -let lexp_error = debug_message error lexp_name lexp_string -let value_fatal = debug_message fatal value_name value_string +let fatal = Log.log_fatal ~section:"ELAB" +let error = Log.log_error ~section:"ELAB" +let warning = Log.log_warning ~section:"ELAB" +let info = Log.log_info ~section:"ELAB" + +let indent_line str = + " > " ^ str +let print_indent_line str = + print_endline (indent_line str) +let print_details to_name to_str elem = + print_indent_line ((to_name elem) ^ ": " ^ (to_str elem)) +let lexp_print_details lexp () = + print_details lexp_name lexp_string lexp +let value_print_details value () = + print_details value_name value_string value + +let lexp_error loc lexp = + error ~loc ~print_action:(lexp_print_details lexp) +let lexp_fatal loc lexp = + fatal ~loc ~print_action:(lexp_print_details lexp) +let value_fatal loc value = + fatal ~loc ~print_action:(value_print_details value) (** Type info returned by elaboration. *) type sform_type = @@ -116,9 +123,9 @@ let sform_default_ectx = ref empty_elab_context let elab_check_sort (ctx : elab_context) lsort var ltp = match (try OL.lexp_whnf lsort (ectx_to_lctx ctx) with e -> - print_string "Exception during whnf of "; - lexp_print lsort; - print_string "\n"; + info ~print_action:(fun _ -> lexp_print lsort; print_newline ()) + ~loc:(lexp_location lsort) + "Exception during whnf of sort:"; raise e) with | Sort (_, _) -> () (* All clear! *) | _ -> let lexp_string e = lexp_string (L.clean e) in @@ -134,15 +141,19 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = let elab_check_proper_type (ctx : elab_context) ltp var = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp with e -> match e with - | Stop_Compilation _ -> raise e - | _ -> print_string "Exception while checking type `"; - lexp_print ltp; - (match var with - | (_, None) -> () - | (_, Some name) - -> print_string ("` of var `" ^ name ^"`\n")); - print_lexp_ctx (ectx_to_lctx ctx); - raise e + | Log.Stop_Compilation _ -> raise e + | _ -> + info + ~print_action:(fun _ -> + print_lexp_ctx (ectx_to_lctx ctx); print_newline () + ) + ~loc:(lexp_location ltp) + ("Exception while checking type `" ^ (lexp_string ltp) ^ "`" + ^ (match var with + | (_, None) -> "" + | (_, Some name) + -> " of var `" ^ name ^ "`")); + raise e let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in @@ -151,30 +162,37 @@ let elab_check_def (ctx : elab_context) var lxp ltype = let lexp_string e = lexp_string (L.clean e) in let ltype' = try OL.check lctx lxp with e -> match e with - (* lexp_error is fatal but Stop_Compilation isn't *) - | Stop_Compilation _ -> raise e - | _ -> lexp_error loc lxp "Error while type-checking"; + | Log.Stop_Compilation _ -> raise e + | _ -> + info + ~print_action:(fun _ -> + lexp_print_details lxp (); print_lexp_ctx (ectx_to_lctx ctx); - raise e in + print_newline () + ) + ~loc + "Error while type-checking"; + raise e in if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' - with e - -> print_string ("Exception while conversion-checking types:\n"); - lexp_print ltype; - print_string (" and "); - lexp_print ltype'; - print_string ("\n"); - lexp_error loc lxp - ("Exception while conversion-checking types " - ^ lexp_string ltype ^ " and " ^ lexp_string ltype'); - raise e) + with e -> + info ~print_action:(lexp_print_details lxp) + ~loc + ("Exception while conversion-checking types: " + ^ lexp_string ltype ^ " and " ^ lexp_string ltype'); + raise e) then elab_check_proper_type ctx ltype var else - (EV.debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [ - (match var with (_, Some n) -> n | _ -> "<anon>") - ^ " = " ^ lexp_string lxp ^ " !: " ^ lexp_string ltype; - " because"; - lexp_string ltype' ^ " != " ^ lexp_string ltype]) + fatal + ~print_action:(fun _ -> + List.iter print_indent_line [ + (match var with (_, Some n) -> n | _ -> "<anon>") + ^ " = " ^ lexp_string lxp ^ " !: " ^ lexp_string ltype; + " because"; + lexp_string ltype' ^ " != " ^ lexp_string ltype + ]) + ~loc + "Type check error: ¡¡ctx_define error!!" let ctx_extend (ctx: elab_context) (var : vname) def ltype = elab_check_proper_type ctx ltype var; @@ -450,7 +468,7 @@ let rec elaborate ctx se ot = and infer (p : sexp) (ctx : elab_context): lexp * ltype = match elaborate ctx p None with - | (_, Checked) -> fatal (sexp_location p) "`infer` got Checked!" + | (_, Checked) -> fatal ~loc:(sexp_location p) "`infer` got Checked!" | (e, Lazy) -> (e, OL.get_type (ectx_to_lctx ctx) e) | (e, Inferred t) -> (e, t) @@ -609,7 +627,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let pat_string p = sexp_string (pexp_u_pat p) in let uniqueness_warn pat = - warning (pexp_pat_location pat) + warning ~loc:(pexp_pat_location pat) ("Pattern " ^ pat_string pat ^ " is a duplicate. It will override previous pattern.") in @@ -920,7 +938,11 @@ and lexp_eval ectx e = ^ track_fv rctx (ectx_to_lctx ectx) e); try EV.eval ee rctx - with exc -> EV.print_eval_trace None; raise exc + with exc -> + let eval_trace = fst (EV.get_trace ()) in + info ~print_action:(fun _ -> EV.print_eval_trace (Some eval_trace)) + "Exception happened during evaluation:"; + raise exc and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option) : value_type = @@ -954,11 +976,11 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp = | Vcommand cmd -> (match (cmd ()) with | Vsexp (sexp) -> sexp - | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a IO sexp")) - | _ -> fatal loc ("Macro `" ^ mname ^ "` should return an IO") + | _ -> fatal ~loc ("Macro `" ^ mname ^ "` should return a IO sexp")) + | _ -> fatal ~loc ("Macro `" ^ mname ^ "` should return an IO") with e -> - fatal loc ("Macro `" ^ mname ^ "` not found") + fatal ~loc ("Macro `" ^ mname ^ "` not found") and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) @@ -981,7 +1003,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) let d = (v', LetDef (i + 1, e), t) in (IMap.add i ((l, Some vname), e, t) map, (grm, ec, Myers.set_nth i d lc, sl)) - | _ -> U.internal_error "Defining same slot!") + | _ -> Log.internal_error "Defining same slot!") defs (IMap.empty, nctx) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in decls, ctx_define_rec ectx decls @@ -1024,8 +1046,8 @@ and lexp_decls_1 let rec lexp_decls_1 sdecls ectx nctx pending_decls pending_defs = match sdecls with | [] -> (if not (SMap.is_empty pending_decls) then - let (s, l) = SMap.choose pending_decls in - error l ("Variable `" ^ s ^ "` declared but not defined!") + let (s, loc) = SMap.choose pending_decls in + error ~loc ("Variable `" ^ s ^ "` declared but not defined!") else assert (pending_defs == [])); [], [], nctx @@ -1037,22 +1059,22 @@ and lexp_decls_1 -> lexp_decls_1 (List.append sdecls' sdecls) ectx nctx pending_decls pending_defs - | Node (Symbol (l, "_:_"), args) :: sdecls + | Node (Symbol (loc, "_:_"), args) :: sdecls (* FIXME: Move this to a "special form"! *) -> (match args with - | [Symbol (l, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (l, Some vname) in + | [Symbol (loc, vname); stp] + -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) let pt_idx = senv_lookup vname nctx in (* Take the previous type annotation. *) let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) - | _ -> U.internal_error "Var not found at its index!" in + | _ -> Log.internal_error "Var not found at its index!" in (* Unify it with the new one. *) let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with | (None | Some (_::_)) - -> lexp_error l ltp + -> lexp_error loc ltp ("New type annotation `" ^ lexp_string ltp ^ "` incompatible with previous `" ^ lexp_string pt ^ "`") @@ -1060,13 +1082,13 @@ and lexp_decls_1 lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else if List.exists (fun ((_, vname'), _) -> vname = vname') pending_defs then - (error l ("Variable `" ^ vname ^ "` already defined!"); + (error ~loc ("Variable `" ^ vname ^ "` already defined!"); lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) else lexp_decls_1 sdecls ectx - (ectx_extend nctx (l, Some vname) ForwardRef ltp) - (SMap.add vname l pending_decls) + (ectx_extend nctx (loc, Some vname) ForwardRef ltp) + (SMap.add vname loc pending_decls) pending_defs - | _ -> error l "Invalid type declaration syntax"; + | _ -> error ~loc "Invalid type declaration syntax"; lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) | Node (Symbol (l, "_=_") as head, args) :: sdecls @@ -1102,7 +1124,7 @@ and lexp_decls_1 lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else - (error l ("`" ^ vname ^ "` defined but not declared!"); + (error ~loc:l ("`" ^ vname ^ "` defined but not declared!"); lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) | [Node (Symbol s, args) as d; body] @@ -1114,7 +1136,7 @@ and lexp_decls_1 :: sdecls) ectx nctx pending_decls pending_defs - | _ -> error l "Invalid definition syntax"; + | _ -> error ~loc:l "Invalid definition syntax"; lexp_decls_1 sdecls ectx nctx pending_decls pending_defs) | Node (Symbol (l, "define-operator"), args) :: sdecls @@ -1129,12 +1151,12 @@ and lexp_decls_1 pending_decls pending_defs | sexp :: sdecls - -> error (sexp_location sexp) "Invalid declaration syntax"; + -> error ~loc:(sexp_location sexp) "Invalid declaration syntax"; lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in (EV.set_getenv nctx; let res = lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in - (stop_on_error (); res)) + (Log.stop_on_error (); res)) and lexp_p_decls (sdecls : sexp list) (ctx : elab_context) : ((vname * lexp * ltype) list list * elab_context) = @@ -1143,14 +1165,14 @@ and lexp_p_decls (sdecls : sexp list) (ctx : elab_context) | _ -> let decls, sdecls, nctx = lexp_decls_1 sdecls ctx ctx SMap.empty [] in let declss, nnctx = lexp_p_decls sdecls nctx in decls :: declss, nnctx in - let res = impl sdecls ctx in (stop_on_error (); res) + let res = impl sdecls ctx in (Log.stop_on_error (); res) and lexp_parse_all (p: sexp list) (ctx: elab_context) : lexp list = let res = List.map (fun pe -> let e, _ = infer pe ctx in e) p in - (stop_on_error (); res) + (Log.stop_on_error (); res) and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = - let e, _ = infer e ctx in (stop_on_error (); e) + let e, _ = infer e ctx in (Log.stop_on_error (); e) (* -------------------------------------------------------------------------- * Special forms implementation @@ -1166,17 +1188,17 @@ and sform_new_attribute ctx loc sargs ot = OL.lexp_close (ectx_to_lctx ctx) ltp, Some AttributeMap.empty), Lazy) - | _ -> fatal loc "new-attribute expects a single Type argument" + | _ -> fatal ~loc "new-attribute expects a single Type argument" and sform_add_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in let table, var, attr = match List.map (lexp_parse_sexp ctx) sargs with | [table; Var((_, Some name), idx); attr] -> table, (n - idx, name), attr - | _ -> fatal loc "add-attribute expects 3 arguments (table; var; attr)" in + | _ -> fatal ~loc "add-attribute expects 3 arguments (table; var; attr)" in let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map, attr_type - | _ -> fatal loc "add-attribute expects a table as first argument" in + | _ -> fatal ~loc "add-attribute expects a table as first argument" in (* FIXME: Type check (attr: type == attr_type) *) let attr' = OL.lexp_close (ectx_to_lctx ctx) attr in @@ -1188,11 +1210,11 @@ and get_attribute ctx loc largs = let ctx_n = get_size ctx in let table, var = match largs with | [table; Var((_, Some name), idx)] -> table, (ctx_n - idx, name) - | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in + | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in let map = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map - | _ -> fatal loc "get-attribute expects a table as first argument" in + | _ -> fatal ~loc "get-attribute expects a table as first argument" in try Some (AttributeMap.find var map) with Not_found -> None @@ -1206,7 +1228,7 @@ and sform_has_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in let table, var = match List.map (lexp_parse_sexp ctx) sargs with | [table; Var((_, Some name), idx)] -> table, (n - idx, name) - | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in + | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map, attr_type @@ -1220,9 +1242,9 @@ and sform_declexpr ctx loc sargs ot = | [Var((_, vn), vi)] -> (match DB.env_lookup_expr ctx ((loc, vn), vi) with | Some lxp -> (lxp, Lazy) - | None -> error loc "no expr available"; + | None -> error ~loc "no expr available"; sform_dummy_ret ctx loc) - | _ -> error loc "declexpr expects one argument"; + | _ -> error ~loc "declexpr expects one argument"; sform_dummy_ret ctx loc @@ -1230,7 +1252,7 @@ let sform_decltype ctx loc sargs ot = match List.map (lexp_parse_sexp ctx) sargs with | [Var((_, vn), vi)] -> (DB.env_lookup_type ctx ((loc, vn), vi), Lazy) - | _ -> error loc "decltype expects one argument"; + | _ -> error ~loc "decltype expects one argument"; sform_dummy_ret ctx loc let builtin_value_types : ltype option SMap.t ref = ref SMap.empty @@ -1246,13 +1268,13 @@ let sform_built_in ctx loc sargs ot = sexp_error loc ("Unknown built-in `" ^ name ^ "`"); BI.add_builtin_cst name bi; (bi, Checked) - | None -> error loc "Built-in's type not provided by context!"; + | None -> error ~loc "Built-in's type not provided by context!"; sform_dummy_ret ctx loc) - | true, _ -> error loc "Wrong Usage of `Built-in`"; + | true, _ -> error ~loc "Wrong Usage of `Built-in`"; sform_dummy_ret ctx loc - | false, _ -> error loc "Use of `Built-in` in user code"; + | false, _ -> error ~loc "Use of `Built-in` in user code"; sform_dummy_ret ctx loc let sform_datacons ctx loc sargs ot = @@ -1282,8 +1304,9 @@ let elab_typecons_arg arg : (arg_kind * vname * sexp option) = -> (elab_colon_to_ak k, (l, Some name), Some e) | Symbol (l, name) -> (Anormal, (l, Some name), None) - | _ -> sexp_print arg; - (sexp_error (sexp_location arg) "Unrecognized formal arg"); + | _ -> sexp_error ~print_action:(fun _ -> sexp_print arg; print_newline ()) + (sexp_location arg) + "Unrecognized formal arg"; (Anormal, (sexp_location arg, None), None) let sform_typecons ctx loc sargs ot = @@ -1411,7 +1434,7 @@ let sform_identifier ctx loc sargs ot = (if not (name = "") then let idx = match mv with | Metavar (idx, _, _) -> idx - | _ -> fatal loc "newMetavar returned a non-Metavar" in + | _ -> fatal ~loc "newMetavar returned a non-Metavar" in rmmap := SMap.add name idx (!rmmap)); (mkSusp mv subst, match ot with Some _ -> Checked | None -> Lazy) @@ -1592,7 +1615,8 @@ let sform_load usr_elctx loc sargs ot = read_file file_name usr_elctx else read_file file_name !sform_default_ectx - | _ -> (error loc "argument to load should be one file name (String)"; !sform_default_ectx) in + | _ -> (error ~loc "argument to load should be one file name (String)"; + !sform_default_ectx) in (* get lexp_context *) let usr_lctx = ectx_to_lctx usr_elctx in @@ -1679,8 +1703,8 @@ let default_ectx let idx = senv_lookup name elctx in let v = mkVar ((dloc, Some name), idx) in BI.set_predef name v) BI.predef_names; - with e -> - warning dloc "Predef not found"; in + with Senv_Lookup_Fail _ -> + warning "Predef not found"; in (* Empty context *) let lctx = empty_elab_context in @@ -1707,7 +1731,10 @@ let default_ectx (fun () -> read_file (btl_folder ^ "/pervasive.typer") lctx) in let _ = sform_default_ectx := ectx in ectx - with (Stop_Compilation _) -> fatal dloc "compilation stopped in default context" + with e -> + error "Compilation stopped in default context"; + Log.print_and_clear_log (); + raise e let default_rctx = EV.from_ectx default_ectx @@ -1723,7 +1750,7 @@ let lexp_expr_str str ctx = List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) lexps; lexps - with Stop_Compilation s -> (print_string s; []) + with Log.Stop_Compilation s -> [] let lexp_decl_str str ctx = try let tenv = default_stt in @@ -1731,7 +1758,7 @@ let lexp_decl_str str ctx = let limit = Some ";" in let sdecls = sexp_parse_str str tenv grm limit in lexp_p_decls sdecls ctx - with Stop_Compilation s -> (print_string s; ([],ctx)) + with Log.Stop_Compilation s -> ([],ctx) (* Eval String @@ -1742,7 +1769,7 @@ let eval_expr_str str lctx rctx = try let lxps = lexp_expr_str str lctx in let elxps = List.map OL.erase_type lxps in EV.eval_all elxps rctx false - with Stop_Compilation s -> (print_string s; []) + with Log.Stop_Compilation s -> [] let eval_decl_str str lctx rctx = let prev_lctx, prev_rctx = lctx, rctx in @@ -1750,5 +1777,5 @@ let eval_decl_str str lctx rctx = let lxps, lctx = lexp_decl_str str lctx in let elxps = (List.map OL.clean_decls lxps) in (EV.eval_decls_toplevel elxps rctx), lctx - with Stop_Compilation s -> (print_string s; prev_rctx, prev_lctx) + with Log.Stop_Compilation s -> (prev_rctx, prev_lctx) ===================================== src/env.ml ===================================== @@ -30,7 +30,6 @@ * * --------------------------------------------------------------------------- *) -open Util (* msg_error *) open Fmt (* make_title, table util *) open Sexp @@ -41,10 +40,10 @@ module L = Lexp module BI = Big_int module DB = Debruijn -let dloc = dummy_location +let dloc = Util.dummy_location -let error loc msg = msg_error "ENV" loc msg; raise (internal_error msg) -let warning loc msg = msg_warning "ENV" loc msg +let fatal = Log.log_fatal ~section:"ENV" +let warning = Log.log_warning ~section:"ENV" let str_idx idx = "[" ^ (string_of_int idx) ^ "]" @@ -81,11 +80,11 @@ let rec value_equal a b = | Vin (c1), Vin (c2) -> c1 = c2 | Vout (c1), Vout (c2) -> c2 = c2 | Vcommand (f1), Vcommand (f2) -> f1 = f2 - | Vundefined, _ | _, Vundefined -> warning dloc "Vundefined"; false - | Vtype e1, Vtype e2 -> warning dloc "Vtype"; false + | Vundefined, _ | _, Vundefined -> warning "Vundefined"; false + | Vtype e1, Vtype e2 -> warning "Vtype"; false | Closure (s1, b1, ctx1), Closure (s2, b2, ctx2) - -> warning dloc "Closure"; + -> warning "Closure"; if (s1 != s2) then false else true | Vcons ((_, ct1), a1), Vcons ((_, ct2), a2) @@ -178,14 +177,14 @@ let get_rte_variable (name: vname) (idx: int) if n1 = n2 then x else ( - error dloc + fatal ("Variable lookup failure. Expected: \"" ^ n2 ^ "[" ^ (string_of_int idx) ^ "]" ^ "\" got \"" ^ n1 ^ "\""))) | _ -> x) with Not_found -> let n = match name with (_, Some n) -> n | _ -> "" in - error dloc ("Variable lookup failure. Var: \"" ^ + fatal ("Variable lookup failure. Var: \"" ^ n ^ "\" idx: " ^ (str_idx idx)) let add_rte_variable (name:vname) (x: value_type) (ctx: runtime_env) @@ -199,7 +198,7 @@ let set_rte_variable idx name (v: value_type) (ctx : runtime_env) = (match (n, name) with | ((_, Some n1), (_, Some n2)) -> if (n1 != n2) then - error dloc ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) + fatal ("Variable's Name must Match: " ^ n1 ^ " vs " ^ n2) | _ -> ()); ref_cell := v ===================================== src/eval.ml ===================================== @@ -82,13 +82,12 @@ let rec_depth trace = List.length b (* eval error are always fatal *) -let error loc msg = - msg_error "EVAL" loc msg; - flush stdout; - raise (internal_error msg) +let error loc ?print_action msg = + Log.log_error ~section:"EVAL" ~loc ?print_action msg; + Log.internal_error msg -let fatal = msg_fatal "EVAL" -let warning = msg_warning "EVAL" +let fatal loc msg = Log.log_fatal ~section:"EVAL" ~loc msg +let warning loc msg = Log.log_warning ~section:"EVAL" ~loc msg (* Print a message that look like this: * @@ -119,7 +118,7 @@ let debug_message error_type type_name type_string loc expr message = (* Print value name followed by the value in itself, finally throw an exception *) let value_fatal = debug_message fatal value_name value_string -let value_error = debug_message error value_name value_string +let value_error = debug_message (error ?print_action:None) value_name value_string let elexp_fatal = debug_message fatal elexp_name elexp_string @@ -341,16 +340,20 @@ let file_read loc depth args_val = match args_val with (* FIXME: Either rename it to "readline" and drop the second arg, * or actually pay attention to the second arg. *) | [Vin channel; Vint n] -> Vstring (input_line channel) - | _ -> List.iter (fun v -> value_print v; print_string "\n") args_val; - error loc "File.read expects an in_channel" + | _ -> error loc ~print_action:(fun _ -> + List.iter (fun v -> value_print v; print_newline ()) args_val; + ) + "File.read expects an in_channel. Actual arguments:" let file_write loc depth args_val = match args_val with | [Vout channel; Vstring msg] -> Vcommand (fun () -> fprintf channel "%s" msg; (* FIXME: This should be the unit value! *) Vundefined) - | _ -> List.iter (fun v -> value_print v) args_val; - error loc "File.write expects an out_channel and a string" + | _ -> error loc ~print_action:(fun _ -> + List.iter (fun v -> value_print v; print_newline ()) args_val; + ) + "File.write expects an out_channel and a string. Actual arguments:" let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) = @@ -470,9 +473,12 @@ and eval_call loc unef i f args = buildbody (arity - nargs - 1), buildctx args Myers.nil) - with Not_found - -> error loc ("Requested Built-in `" ^ name ^ "` does not exist") - | e -> error loc ("Exception thrown from primitive `" ^ name ^"`")) + with + | Not_found -> + error loc ("Requested Built-in `" ^ name ^ "` does not exist") + | e -> + warning loc ("Exception thrown from primitive `" ^ name ^"`"); + raise e) | Vtype e, _ (* We may call a Vlexp e.g. for "x = Map Int String". @@ -902,19 +908,27 @@ let array_empty loc depth args_val = match args_val with let test_fatal loc depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> Util.msg_user_fatal section loc msg) + Vcommand (fun () -> + Log.print_entry + (Log.mkEntry Log.Fatal ~kind:"(Unit test fatal)" ~loc ~section msg); + Log.user_error msg + ) | _ -> error loc "Test.fatal takes two String as argument" let test_warning loc depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> Util.msg_user_warning section loc msg; - tunit) + Vcommand (fun () -> + Log.print_entry + (Log.mkEntry Log.Warning ~kind:"(Unit test warning)" ~loc ~section msg); + tunit) | _ -> error loc "Test.warning takes two String as argument" let test_info loc depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> Util.msg_user_info section loc msg; - tunit) + Vcommand (fun () -> + Log.print_entry + (Log.mkEntry Log.Info ~kind:"(Unit test Info)" ~loc ~section msg); + tunit) | _ -> error loc "Test.info takes two String as argument" let test_location loc depth args_val = match args_val with @@ -1049,10 +1063,14 @@ let eval lxp ctx = eval lxp ctx ([], []) let debug_eval lxp ctx = try eval lxp ctx with e -> ( - print_rte_ctx (!global_eval_ctx); - print_eval_trace None; - raise e) - + let ectx = !global_eval_ctx in + let eval_trace = fst (get_trace ()) in + Log.log_info ~section:"EVAL" ~print_action:(fun _ -> + print_rte_ctx ectx; + print_eval_trace (Some eval_trace) + ) + "Exception occured during evaluation in the following context:"; + raise e) let eval_decls decls ctx = eval_decls decls ctx ([], []) ===================================== src/fmt.ml ===================================== @@ -156,3 +156,6 @@ let yellow = "\x1b[33m" let magenta = "\x1b[35m" let cyan = "\x1b[36m" let reset = "\x1b[0m" + +let color_string color str = + color ^ str ^ reset ===================================== src/inverse_subst.ml ===================================== @@ -169,11 +169,11 @@ let inverse (s: Lexp.subst) : Lexp.subst option = | Some s1 -> if is_identity (Lexp.scompose s s1) || is_identity (Lexp.scompose s1 s) then () - else (print_string ("Subst-inversion-bug: " - ^ subst_string s ^ " ∘ " - ^ subst_string s1 ^ " == " - ^ subst_string (Lexp.scompose s1 s) - ^ " !!\n")) + else (Log.log_debug ("Subst-inversion-bug: " + ^ subst_string s ^ " ∘ " + ^ subst_string s1 ^ " == " + ^ subst_string (Lexp.scompose s1 s) + ^ " !!\n")) | _ -> ()); res ===================================== src/lexer.ml ===================================== @@ -45,7 +45,7 @@ let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos (* The returned Sexp may not be a Node. *) : sexp * pretoken list * bytepos * charpos = match pts with - | [] -> (internal_error "No next token!") + | [] -> (Log.internal_error "No next token!") | (Preblock (sl, bpts, el) :: pts) -> (Block (sl, bpts, el), pts, 0, 0) | (Prestring (loc, str) :: pts) -> (String (loc, str), pts, 0, 0) | (Pretoken ({file;line;column;docstr}, name) :: pts') ===================================== src/lexp.ml ===================================== @@ -166,7 +166,7 @@ let metavar_table = ref (U.IMap.empty : meta_subst) let metavar_lookup (id : meta_id) : metavar_info = try U.IMap.find id (!metavar_table) with Not_found - -> U.msg_fatal "LEXP" U.dummy_location "metavar lookup failure!" + -> Log.log_fatal ~section:"LEXP" "metavar lookup failure!" (********************** Hash-consing **********************) @@ -207,18 +207,18 @@ let mkCall (f, es) let mkSLlub' (e1, e2) = match (e1, e2) with | (SortLevel SLz, _) | (_, SortLevel SLz) - -> U.msg_fatal "internal" U.dummy_location "lub of SLz" + -> Log.log_fatal ~section:"internal" "lub of SLz" | (SortLevel (SLsucc _), SortLevel (SLsucc _)) - -> U.msg_fatal "internal" U.dummy_location "lub of two SLsucc" + -> Log.log_fatal ~section:"internal" "lub of two SLsucc" | ((SortLevel _ | Var _ | Metavar _ | Susp _), (SortLevel _ | Var _ | Metavar _ | Susp _)) -> SLlub (e1, e2) - | _ -> U.msg_fatal "internal" U.dummy_location "SLlub of non-level" + | _ -> Log.log_fatal ~section:"internal" "SLlub of non-level" let mkSLsucc e = match e with | SortLevel _ | Var _ | Metavar _ | Susp _ -> SLsucc e - | _ -> U.msg_fatal "internal" U.dummy_location "SLsucc of non-level" + | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level" (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. @@ -657,20 +657,29 @@ let debug_ppctx = ref ( ("print_implicit", Bool (true)); ("separate_decl" , Bool (false) );]) -let pp_pretty ctx = match SMap.find "pretty" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_type ctx = match SMap.find "print_type" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_dbi ctx = match SMap.find "print_dbi" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_size ctx = match SMap.find "indent_size" ctx with Int i -> i | _ -> U.typer_unreachable "" -let pp_color ctx = match SMap.find "color" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_decl ctx = match SMap.find "separate_decl" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_indent ctx = match SMap.find "indent_level" ctx with Int i -> i | _ -> U.typer_unreachable "" -let pp_parent ctx = match SMap.find "parent" ctx with Expr e -> e | _ -> U.typer_unreachable "" -let pp_meta ctx = match SMap.find "metavar" ctx with Expr e -> e | _ -> U.typer_unreachable "" -let pp_grammar ctx = match SMap.find "grammar" ctx with Predtl p -> p | _ -> U.typer_unreachable "" -let pp_colsize ctx = match SMap.find "col_size" ctx with Int i -> i | _ -> U.typer_unreachable "" -let pp_colmax ctx = match SMap.find "col_max" ctx with Int i -> i | _ -> U.typer_unreachable "" -let pp_erasable ctx = match SMap.find "print_erasable" ctx with Bool b -> b | _ -> U.typer_unreachable "" -let pp_implicit ctx = match SMap.find "print_implicit" ctx with Bool b -> b | _ -> U.typer_unreachable "" +let smap_bool s ctx = + match SMap.find s ctx with Bool b -> b | _ -> failwith "Unreachable" +and smap_int s ctx = + match SMap.find s ctx with Int i -> i | _ -> failwith "Unreachable" +and smap_lexp s ctx = + match SMap.find s ctx with Expr e -> e | _ -> failwith "Unreachable" +and smap_predtl s ctx = + match SMap.find s ctx with Predtl tl -> tl | _ -> failwith "Unreachable" + +let pp_pretty = smap_bool "pretty" +let pp_type = smap_bool "print_type" +let pp_dbi = smap_bool "print_dbi" +let pp_size = smap_int "indent_size" +let pp_color = smap_bool "color" +let pp_decl = smap_bool "separate_decl" +let pp_indent = smap_int "indent_level" +let pp_parent = smap_lexp "parent" +let pp_meta = smap_lexp "metavar" +let pp_grammar = smap_predtl "grammar" +let pp_colsize = smap_int "col_size" +let pp_colmax = smap_int "col_max" +let pp_erasable = smap_bool "print_erasable" +let pp_implicit = smap_bool "print_implicit" let set_col_size p ctx = SMap.add "col_size" (Int p) ctx let add_col_size p ctx = set_col_size ((pp_colsize ctx) + p) ctx ===================================== src/log.ml ===================================== @@ -0,0 +1,216 @@ +(* log.ml --- User Errors/Warnings log for Typer. -*- coding: utf-8 -*- + +Copyright (C) 2019 Free Software Foundation, Inc. + +Author: Jean-Alexandre Barszcz <jalex_b(a)hotmail.com> +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 Util + +(* LOGGING LEVELS *) + +type log_level = Nothing | Fatal | Error | Warning | Info | Debug + +let int_of_level lvl = + match lvl with + | Nothing -> -1 (* We might not want to print anything during testing *) + | Fatal -> 0 | Error -> 1 | Warning -> 2 | Info -> 3 | Debug -> 4 + +let level_of_int i = + match i with + | _ when i < 0 -> Nothing + | 0 -> Fatal | 1 -> Error | 2 -> Warning | 3 -> Info + | _ -> Debug + +let string_of_level lvl = + match lvl with + | Nothing -> "Nothing" + | Fatal -> "Fatal" + | Error -> "Error" + | Warning -> "Warning" + | Info -> "Info" + | Debug -> "Debug" + +let level_of_string str = + match Util.string_uppercase str with + | "NOTHING" -> Nothing + | "FATAL" -> Fatal + | "ERROR" -> Error + | "WARNING" -> Warning + | "INFO" -> Info + | "DEBUG" -> Debug + | _ -> invalid_arg ("`"^str^"` is not a logging level") + +let level_color lvl = + match lvl with + | Nothing -> None + | Fatal -> Some Fmt.red + | Error -> Some Fmt.red + | Warning -> Some Fmt.yellow + | Info -> Some Fmt.cyan + | Debug -> Some Fmt.magenta + +(* LOGGING CONFIGURATION *) + +type log_config = { + mutable level : log_level; + mutable print_at_log : bool; + mutable print_in_reverse : bool; + mutable color : bool; + } + +let typer_log_config = { + level = Warning; + print_at_log = false; + print_in_reverse = false; + color = true; + } + +(* LOG DEFINITION *) + +type log_entry = { + level : log_level; + kind : string option; + section : string option; + print_action : (unit -> unit) option; + loc : location option; + msg : string; + } + +type log = log_entry list + +let empty_log = [] + +let typer_log = ref empty_log + +(* PRIVATE OPERATIONS *) + +let mkEntry level ?kind ?section ?print_action ?loc msg = + {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 + | None -> 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) ^ " " + ^ msg) + +let print_entry entry = + print_endline (string_of_log_entry entry); + match entry.print_action with + | Some f -> f () + | None -> () + +let log_entry (entry : log_entry) = + if (entry.level <= typer_log_config.level) + then ( + log_push entry; + if (typer_log_config.print_at_log) + then + (print_entry entry; + flush stdout) + ) + +let count_msgs (lvlp : log_level -> bool) = + let count_step count {level} = + if lvlp level then count + 1 else count + in + List.fold_left count_step 0 !typer_log + +let error_count () = count_msgs (fun level -> level <= Error) +let warning_count () = count_msgs (fun level -> level = Warning) + +(* PUBLIC INTERFACE *) + +let set_typer_log_level lvl = + typer_log_config.level <- lvl + +let set_typer_log_level_str str = + try set_typer_log_level (level_of_int (int_of_string str)) + with + _ -> set_typer_log_level (level_of_string str) + +let increment_log_level () = + typer_log_config.level + |> int_of_level + |> (+) 1 + |> level_of_int + |> set_typer_log_level + +let clear_log () = typer_log := empty_log + +let print_log () = + let reverse = typer_log_config.print_in_reverse in + let l = if reverse then !typer_log else List.rev !typer_log in + List.iter print_entry l + +let print_and_clear_log () = + print_log (); clear_log () + +let log_msg level ?kind ?section ?print_action ?loc msg = + log_entry (mkEntry level ?kind ?section ?print_action ?loc msg) + +exception Internal_error of string +let internal_error s = raise (Internal_error s) + +exception User_error of string +let user_error s = raise (User_error s) + +exception Stop_Compilation of string +let stop_compilation s = raise (Stop_Compilation s) + +let log_fatal ?section ?print_action ?loc m = + log_msg Fatal ~kind:"[X] Fatal " ?section ?print_action ?loc m; + internal_error "Compiler Fatal Error" +let log_error = log_msg Error ?kind:None +let log_warning = log_msg Warning ?kind:None +let log_info = log_msg Info ?kind:None +let log_debug = log_msg Debug ?kind:None + +let stop_on_error () = + let count = error_count () in + if (0 < count) then + stop_compilation + ("Compiler stopped after: "^(string_of_int count)^" errors\n") + +let stop_on_warning () = + stop_on_error (); + let count = warning_count () in + if (0 < count) then + stop_compilation + ("Compiler stopped after: "^(string_of_int count)^" warnings\n") + +(* Compiler Internal Debug print *) +let debug_msg expr = + if Debug <= typer_log_config.level then (print_string expr; flush stdout) + +let not_implemented_error () = internal_error "not implemented" ===================================== src/opslexp.ml ===================================== @@ -38,6 +38,9 @@ module S = Subst (* module L = List *) module DB = Debruijn +let error_tc = Log.log_error ~section:"TC" +let warning_tc = Log.log_warning ~section:"TC" + (* `conv_erase` is supposed to be safe according to the ICC papers. *) let conv_erase = true (* Makes conv ignore erased terms. *) @@ -161,7 +164,7 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = -> match default with | Some (v,default) -> lexp_whnf (push_susp default (S.substitute e')) ctx - | _ -> U.msg_error "WHNF" l + | _ -> Log.log_error ~section:"WHNF" ~loc:l ("Unhandled constructor " ^ name ^ "in case expression"); mkCase (l, e, rt, branches, default) in @@ -399,17 +402,17 @@ let rec check'' erased ctx e = let check = check'' in let assert_type ctx e t t' = if conv_p ctx t t' then () - else (U.msg_error "TC" (lexp_location e) + else (error_tc ~loc:(lexp_location e) ("Type mismatch for " ^ lexp_string (L.clean e) ^ " : " ^ lexp_string (L.clean t) ^ " != " ^ lexp_string (L.clean t')); - (* U.internal_error "Type mismatch" *)) in + (* Log.internal_error "Type mismatch" *)) in let check_type erased ctx t = let s = check erased ctx t in (match lexp_whnf s ctx with | Sort _ -> () - | _ -> U.msg_error "TC" (lexp_location t) + | _ -> error_tc ~loc:(lexp_location t) ("Not a proper type: " ^ lexp_string t)); (* FIXME: return the `sort` rather than the surrounding `lexp`! *) s in @@ -419,7 +422,7 @@ let rec check'' erased ctx e = | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) - -> (U.msg_error "TC" (lexp_location e) "Unsupported immediate value!"; + -> (error_tc ~loc:(lexp_location e) "Unsupported immediate value!"; DB.type_int) | SortLevel SLz -> DB.type_level | SortLevel (SLsucc e) @@ -440,8 +443,8 @@ let rec check'' erased ctx e = mkSort (l, Stype (mkSortLevel (SLsucc e))) | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) - -> ((* U.msg_error "TC" (lexp_location e) "Reached unreachable sort!"; - * U.internal_error "Reached unreachable sort!"; *) + -> ((* error_tc ~loc:(lexp_location e) "Reached unreachable sort!"; + * Log.internal_error "Reached unreachable sort!"; *) DB.sort_omega) | Builtin (_, t, _) -> let _ = check_type DB.set_empty Myers.nil t in @@ -450,7 +453,7 @@ let rec check'' erased ctx e = (* FIXME: Check recursive references. *) | Var (((l, name), idx) as v) -> if DB.set_mem idx erased then - U.msg_error "TC" l + error_tc ~loc:l ("Var `" ^ maybename name ^ "`" ^ " can't be used here, because it's `erasable`"); lookup_type ctx v @@ -483,14 +486,14 @@ let rec check'' erased ctx e = match sort_compose ctx l ak k1 k2 with | SortResult k -> k | SortInvalid - -> U.msg_error "TC" l "Invalid arrow: inner TypelLevel argument"; + -> error_tc ~loc:l "Invalid arrow: inner TypelLevel argument"; mkSort (l, StypeOmega) | SortK1NotType - -> (U.msg_error "TC" (lexp_location t1) + -> (error_tc ~loc:(lexp_location t1) "Not a proper type"; mkSort (l, StypeOmega)) | SortK2NotType - -> (U.msg_error "TC" (lexp_location t2) + -> (error_tc ~loc:(lexp_location t2) "Not a proper type"; mkSort (l, StypeOmega))) | Lambda (ak, ((l,_) as v), t, e) @@ -508,12 +511,12 @@ let rec check'' erased ctx e = match lexp_whnf ft ctx with | Arrow (ak', v, t1, l, t2) -> if not (ak == ak') then - (U.msg_error "TC" (lexp_location arg) + (error_tc ~loc:(lexp_location arg) "arg kind mismatch"; ()) else (); assert_type ctx arg t1 at; mkSusp t2 (S.substitute arg) - | _ -> (U.msg_error "TC" (lexp_location arg) + | _ -> (error_tc ~loc:(lexp_location arg) ("Calling a non function (type = " ^ lexp_string ft ^ ")!"); ft)) @@ -538,14 +541,15 @@ let rec check'' erased ctx e = (* We need to unshift because the final type * cannot refer to the fields! *) (mkSusp level' (L.sunshift n)) - | tt -> U.msg_error "TC" (lexp_location t) - ("Field type " - ^ lexp_string t - ^ " is not a Type! (" - ^ lexp_string tt ^")"); - DB.print_lexp_ctx ictx; - (* U.internal_error "Oops"; *) - level), + | tt -> error_tc ~loc:(lexp_location t) + ~print_action:(fun _ -> + DB.print_lexp_ctx ictx; print_newline () + ) + ("Field type " + ^ lexp_string t + ^ " is not a Type! (" + ^ lexp_string tt ^")"); + level), DB.lctx_extend ictx v Variable t, DB.set_sink 1 erased, n + 1)) @@ -578,7 +582,7 @@ let rec check'' erased ctx e = (* We don't check aarg's type, because we assume that `check` * returns a valid type. *) -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (U.msg_error "TC" l + | _,_ -> (error_tc ~loc:l "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in SMap.iter @@ -595,7 +599,7 @@ let rec check'' erased ctx e = (S.cons (Var (vdef, 0)) (S.mkShift s 1)) vdefs fieldtypes - | _,_ -> (U.msg_error "TC" l + | _,_ -> (error_tc ~loc:l "Wrong number of args to constructor!"; (erased, ctx)) in let (nerased, nctx) = mkctx erased ctx s vdefs fieldtypes in @@ -607,15 +611,15 @@ let rec check'' erased ctx e = (match default with | Some (v, d) -> if diff <= 0 then - U.msg_warning "TC" l "Redundant default clause"; + warning_tc ~loc:l "Redundant default clause"; let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in assert_type nctx d (mkSusp ret (S.shift 1)) (check (DB.set_sink 1 erased) nctx d) | None -> if diff > 0 then - U.msg_error "TC" l ("Non-exhaustive match: " + error_tc ~loc:l ("Non-exhaustive match: " ^ string_of_int diff ^ " cases missing")) - | _,_ -> U.msg_error "TC" l "Case on a non-inductive type!"); + | _,_ -> error_tc ~loc:l "Case on a non-inductive type!"); ret | Cons (t, (l, name)) -> (match lexp_whnf t ctx with @@ -643,10 +647,10 @@ let rec check'' erased ctx e = buildtype fargs) in buildtype fargs with Not_found - -> (U.msg_error "TC" l + -> (error_tc ~loc:l ("Constructor \"" ^ name ^ "\" does not exist"); DB.type_int)) - | _ -> (U.msg_error "TC" (lexp_location e) + | _ -> (error_tc ~loc:(lexp_location e) ("Cons of a non-inductive type: " ^ lexp_string t); DB.type_int)) @@ -658,7 +662,7 @@ let rec check'' erased ctx e = let check' ctx e = let res = check'' DB.set_empty ctx e in - (U.stop_on_error (); res) + (Log.stop_on_error (); res) let check = check' @@ -917,7 +921,7 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Sort _ -> E.Type lxp (* Still useful to some extent. *) | L.Inductive(l, label, _, _) -> E.Type lxp - | L.Metavar _ -> U.internal_error "Metavar in erase_type" + | L.Metavar _ -> Log.internal_error "Metavar in erase_type" and filter_arg_list lst = let rec filter_arg_list lst acc = @@ -955,7 +959,7 @@ and clean_map cases = (** Turning a set of declarations into an object. **) let ctx2tup ctx nctx = - (*U.debug_msg ("Entering ctx2tup\n");*) + (*Log.debug_msg ("Entering ctx2tup\n");*) assert (M.length nctx >= M.length ctx && ctx == M.nthcdr (M.length nctx - M.length ctx) nctx); let rec get_blocs nctx blocs = @@ -973,7 +977,7 @@ let ctx2tup ctx nctx = let type_label = (loc, "record") in let offset = List.length types in let types = List.rev types in - (*U.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*) + (*Log.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*) Call (Cons (Inductive (loc, type_label, [], SMap.add cons_name (List.map (fun (oname, t) ===================================== src/pexp.ml ===================================== @@ -25,7 +25,7 @@ open Sexp (* Symbol *) open Lexer open Grammar -let pexp_error = msg_error "PEXP" +let pexp_error loc = Log.log_error ~section:"PEXP" ~loc (*************** The Pexp Parser *********************) ===================================== src/prelexer.ml ===================================== @@ -22,7 +22,7 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) open Util -let prelexer_error = msg_error "PRELEXER" +let prelexer_error loc = Log.log_error ~section:"PRELEXER" ~loc type pretoken = | Pretoken of location * string ===================================== src/sexp.ml ===================================== @@ -24,7 +24,8 @@ open Util open Prelexer open Grammar -let sexp_error = msg_error "SEXP" +let sexp_error ?print_action loc msg = + Log.log_error ~section:"SEXP" ?print_action ~loc msg type integer = (* Num.num *) int type symbol = location * string @@ -119,7 +120,7 @@ let rec sexp_parse (g : grammar) (rest : sexp list) let sexp_parse = sexp_parse g in let rec compose_symbol (ss : symbol list) = match ss with - | [] -> (internal_error "empty operator!") + | [] -> (Log.internal_error "empty operator!") | (l,_)::_ -> (l, String.concat "_" (List.map (fun (_,s) -> s) (List.rev ss))) in @@ -201,19 +202,19 @@ let sexp_parse_all grm tokens limit : sexp * token list = | Some token -> match SMap.find token grm with | (Some ll, Some _) -> ll + 1 - | _ -> (internal_error ("Can't find level of \""^token^"\"")) + | _ -> (Log.internal_error ("Can't find level of \""^token^"\"")) in let (e, rest) = sexp_parse grm tokens level [] [] [] in let se = match e with | Node (Symbol (_, ""), [e]) -> e | Node (Symbol (_, ""), e::es) -> Node (e, es) - | _ -> (internal_error "Didn't find a toplevel") in + | _ -> (Log.internal_error "Didn't find a toplevel") in match rest with | [] -> (se,rest) | Symbol (l,t) :: rest -> if not (Some t = limit) then sexp_error l ("Stray closing token: \"" ^ t ^ "\""); (se,rest) - | _ -> (internal_error "Stopped parsing before the end!") + | _ -> (Log.internal_error "Stopped parsing before the end!") (* "sexp_p" is for "parsing" and "sexp_u" is for "unparsing". *) ===================================== src/unification.ml ===================================== @@ -27,6 +27,8 @@ module DB = Debruijn (** Provide unify function for unifying two Lambda-Expression *) +let log_info = Log.log_info ~section:"UNIF" + (* :-( *) let global_last_metavar = ref (-1) (*The first metavar is 0*) @@ -45,7 +47,7 @@ let associate (id: meta_id) (lxp: lexp) (subst: meta_subst) : meta_subst = U.IMap.add id (MVal lxp) subst let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with - | MVal _ -> U.internal_error + | MVal _ -> Log.internal_error "Checking occurrence of an instantiated metavar!!" | MVar (sl, _, _) -> let rec oi e = match e with @@ -57,7 +59,7 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | Sort (_, (StypeOmega | StypeLevel)) -> false | Builtin _ -> false | Var (_, i) -> false - | Susp (e, s) -> U.internal_error "`e` should be \"clean\" here!?" + | Susp (e, s) -> Log.internal_error "`e` should be \"clean\" here!?" (* ; oi (push_susp e s) *) | Let (_, defs, e) -> List.fold_left (fun o (_, e, t) -> o || oi e || oi t) (oi e) defs @@ -81,7 +83,7 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | Metavar (id', _, name) when id' = id -> true | Metavar (id', _, _) -> (match metavar_lookup id' with - | MVal e -> U.internal_error "`e` should be \"clean\" here!?" + | MVal e -> Log.internal_error "`e` should be \"clean\" here!?" (* ; oi e *) | MVar (sl', t, cl) -> if sl' > sl then @@ -227,17 +229,16 @@ and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) : return_type = let unif idx s lxp = let t = match metavar_lookup idx with - | MVal _ -> U.internal_error + | MVal _ -> Log.internal_error "`lexp_whnf` returned an instantiated metavar!!" | MVar (_, t, _) -> push_susp t s in match Inverse_subst.apply_inv_subst lxp s with | exception Inverse_subst.Not_invertible - -> print_string "Unification of metavar failed:\n "; - print_string ("?[" ^ subst_string s ^ "]"); - print_string "\nAgainst:\n "; - lexp_print lxp; - print_string "\n"; - None + -> log_info ?loc:None ("Unification of metavar failed:\n " + ^ "?[" ^ subst_string s ^ "]" + ^ "\nAgainst:\n " + ^ lexp_string lxp ^ "\n"); + None | lxp' when occurs_in idx lxp' -> None | lxp' -> metavar_table := associate idx lxp' (!metavar_table); @@ -245,11 +246,12 @@ and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) | Some [] as r -> r (* FIXME: Let's ignore the error for now. *) | _ - -> print_string ("Unification of metavar type failed:\n " - ^ lexp_string (Lexp.clean t) ^ " != " - ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) - ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); - Some [] in + -> log_info ?loc:None + ("Unification of metavar type failed:\n " + ^ lexp_string (Lexp.clean t) ^ " != " + ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) + ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); + Some [] in match lxp2 with | Metavar (idx2, s2, _) -> if idx = idx2 then ===================================== src/util.ml ===================================== @@ -51,114 +51,6 @@ let loc_string loc = let loc_print loc = print_string (loc_string loc) -(* - * -1 - Nothing (* During testing we may want to produce errors *) - * 0 - Fatal - * 1 - Error - * 2 - Warning - * 3 - Info - *) - -let typer_verbose = ref 20 - -exception Internal_error of string -let internal_error s = raise (Internal_error s) - -exception Unreachable_error of string -let typer_unreachable s = raise (Unreachable_error s) - -exception User_error of string -let user_error s = raise (User_error s) - -exception Stop_Compilation of string -let stop_compilation s = raise (Stop_Compilation s) - -(* `error list * warning list` both of type `level * kind * section * loc * msg` *) -type error_log_type = ((int * string * string * location * string) list * - (int * string * string * location * string) list) - -let empty_error_log : error_log_type = ([],[]) - -let error_log = ref empty_error_log - -let error_count () : int = let errors, _ = !error_log in - List.length errors - -let warning_count () : int = let _, warnings = !error_log in - List.length warnings - -let new_error lvl kind section loc msg = let errors, warnings = !error_log in - error_log := ((lvl,kind,section,loc,msg)::errors,warnings) - -let new_warning lvl kind section loc msg = let errors, warnings = !error_log in - error_log := (errors,(lvl,kind,section,loc,msg)::warnings) - -let reset_error_log () = error_log := empty_error_log - -(* Section is the name of the compilation step [for debugging] *) -(* 'prerr' output is ugly *) -let msg_message (error : bool) lvl kind section (loc: location) msg = - let message = (loc.file - ^ ":" ^ string_of_int loc.line - ^ ":" ^ string_of_int loc.column - ^ ":" ^ kind - ^ (if section = "" then " " else "(" ^ section ^ ") ") - ^ msg ^ "\n") in - - if error then - new_error lvl kind section loc msg - else - new_warning lvl kind section loc msg; - - if lvl <= !typer_verbose then - print_string message - else () - -let stop_on_error () = if (0 < (error_count ())) then - (let count = error_count () in - reset_error_log (); - stop_compilation - ("Compiler stopped after: "^(string_of_int count)^" error\n")) - else () - -let stop_on_warning () = (stop_on_error (); - if (0 < (warning_count ())) then - let count = warning_count () in - reset_error_log (); - stop_compilation - ("Compiler stopped after: "^(string_of_int count)^" warning\n") - else ()) - -let catch_error () = try stop_on_error () - with e -> match e with - | Stop_Compilation msg -> print_string msg - | _ -> () - -let msg_fatal s l m = - msg_message false 0 "[X] Fatal " s l m; - flush stdout; - reset_error_log (); - internal_error "Compiler Fatal Error" - -let msg_error = msg_message true 1 "Error:" -let msg_warning = msg_message false 2 "Warning:" -let msg_info = msg_message false 3 "Info:" - -let msg_user_fatal s l m = - msg_message true 1 "(Unit test fatal):" s l m; - flush stdout; - reset_error_log (); - user_error "User Fatal Error" - -let msg_user_warning = msg_message false 2 "(Unit test warning):" -let msg_user_info = msg_message false 3 "(Unit test info):" - -(* Compiler Internal Debug print *) -let debug_msg expr = - if 4 <= !typer_verbose then (print_string expr; flush stdout) else () - -let not_implemented_error () = internal_error "not implemented" - let string_implode chars = String.concat "" (List.map (String.make 1) chars) let string_sub str b e = String.sub str b (e - b) @@ -214,3 +106,13 @@ 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/utest_lib.ml ===================================== @@ -76,7 +76,7 @@ let global_ftitle = ref "" let set_verbose lvl = global_verbose_lvl := lvl; - (if lvl >= 3 then U.typer_verbose := 20 else U.typer_verbose := (-1)) + Log.set_typer_log_level (if lvl >= 3 then Log.Debug else Log.Nothing) let arg_defs = [ ("--verbose=", View it on GitLab: https://gitlab.com/monnier/typer/compare/5c7f8365dbe0557a3060457f4743970e9b… -- View it on GitLab: https://gitlab.com/monnier/typer/compare/5c7f8365dbe0557a3060457f4743970e9b… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Octobre 2019