Mars 2023 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][gensym-without-spaces] Escape charaters like spaces when printing a symbol or vname.
by Simon Génier (＠ilovemonoids) 25 Mar '23

25 Mar '23

Simon Génier pushed to branch gensym-without-spaces at Stefan / Typer Commits: 01dbc11d by Simon Génier at 2023-03-25T12:28:15-04:00 Escape charaters like spaces when printing a symbol or vname. - - - - - 4 changed files: - src/grammar.ml - src/sexp.ml - src/util.ml - tests/sexp_test.ml Changes: ===================================== src/grammar.ml ===================================== @@ -46,6 +46,9 @@ let find (name : string) (Grammar (ps) : t) : int option * int option = try SMap.find name ps with | Not_found -> (None, None) +let separate_chars = + CSet.of_list [','; '('; ')'; ';'] + (* A token_end array indicates the few chars which are separate tokens, * even if not surrounded by spaces, such as '(', ')', and ';'. * It also indicates which chars are "inner" operators, i.e. those chars @@ -54,13 +57,10 @@ let find (name : string) (Grammar (ps) : t) : int option * int option = type char_kind = | CKnormal | CKseparate | CKinner of int type token_env = char_kind array let default_stt : token_env = - let stt = Array.make 256 CKnormal - in stt.(Char.code ';') <- CKseparate; - stt.(Char.code ',') <- CKseparate; - stt.(Char.code '(') <- CKseparate; - stt.(Char.code ')') <- CKseparate; - stt.(Char.code '.') <- CKinner 5; - stt + let stt = Array.make 256 CKnormal in + CSet.iter (fun c -> stt.(Char.code c) <- CKseparate) separate_chars; + stt.(Char.code '.') <- CKinner 5; + stt (* default_grammar is auto-generated from typer-smie-grammar via: ===================================== src/sexp.ml ===================================== @@ -26,6 +26,17 @@ open Prelexer let sexp_error ?print_action loc fmt = Log.log_error ~section:"SEXP" ?print_action ~loc fmt +(** Prints an identifier in a way that reading it back will yield the same + identifier. Spaces, inner operators like ‘.’, and separate characters like + ‘,’ are escaped. *) +let pp_print_id (f : Format.formatter) (name : string) : unit = + let pp_print_escaped_char c = + if c = '.' || c = ' ' || CSet.mem c Grammar.separate_chars then + Format.pp_print_char f '\\'; + Format.pp_print_char f c + in + String.iter pp_print_escaped_char name + module Sym = struct type t = Source.Location.t * string @@ -53,7 +64,10 @@ module Sym = struct && name l = name r let pp_print (f : Format.formatter) (_, name : t) : unit = - Format.pp_print_string f name + pp_print_id f name + + let to_string : t -> string = + Format.asprintf "%a" pp_print end type symbol = Sym.t @@ -105,7 +119,7 @@ let string_of_vname ?(default : string = "<anon>") : vname -> string = function let pp_print_vname ?(default : string option) (f : Format.formatter) (name : vname) : unit = - Format.pp_print_string f (string_of_vname ?default name) + pp_print_id f (string_of_vname ?default name) (********************** Sexp tests **********************) ===================================== src/util.ml ===================================== @@ -22,6 +22,7 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) module SMap = Map.Make(String) module IMap = Map.Make(Int) +module CSet = Set.Make(Char) type location = Source.Location.t let dummy_location = Source.Location.dummy ===================================== tests/sexp_test.ml ===================================== @@ -87,5 +87,33 @@ let _ = "x = 4 : Int" "(_=_ x (_:_ 4 Int))" +let () = + add_test + "SEXP" + "Spaces are escaped in symbols" + (fun () -> + if + "Laura Palmer" + |> Sym.intern ~location:Source.Location.dummy + |> Sym.to_string + = "Laura\\ Palmer" + then + success + else failure) + +let () = + add_test + "SEXP" + "Dots are escaped in symbols" + (fun () -> + if + "DaleB.Cooper" + |> Sym.intern ~location:Source.Location.dummy + |> Sym.to_string + = "DaleB\\.Cooper" + then + success + else failure) + (* run all tests *) let _ = run_all () View it on GitLab: https://gitlab.com/monnier/typer/-/commit/01dbc11da02b8e5e5896659d712e6e1ab… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/01dbc11da02b8e5e5896659d712e6e1ab… You're receiving this email because of your account on gitlab.com.

2 1

[Git][monnier/typer][simon--pp-print-lctx] Dump lctx from typer.exe rather than debug_util.exe.
by Simon Génier (＠ilovemonoids) 24 Mar '23

24 Mar '23

Simon Génier pushed to branch simon--pp-print-lctx at Stefan / Typer Commits: 023768b1 by Simon Génier at 2023-03-24T17:03:13-04:00 Dump lctx from typer.exe rather than debug_util.exe. - - - - - 3 changed files: - debug_util.ml - src/lctx.ml - typer.ml Changes: ===================================== debug_util.ml ===================================== @@ -68,10 +68,6 @@ let get_p_option name = let arg_defs = [ ("-typecheck", Arg.Unit (add_p_option "typecheck"), " Enable type checking"); - - (* Debug *) - ("-lctx", - Arg.Unit (add_p_option "lctx"), " Print lexp context"); ("-rctx", Arg.Unit (add_p_option "rctx"), " Print runtime context"); ("-all", @@ -144,9 +140,6 @@ let main () = print_string (" " ^ (make_line '-' 76)); print_string "\n";)); - (if (get_p_option "lctx") then( - Lctx.print (ectx_to_lctx nctx); print_string "\n")); - (* Type erasure *) let _, clean_lxp = List.fold_left_map OL.clean_decls (ectx_to_lctx nctx) lexps ===================================== src/lctx.ml ===================================== @@ -113,11 +113,15 @@ let summarize ~(around : int) (lctx : t) : unit = print_endline "This context was trucated. Pass the option -Vfull-lctx to view it in full." (** Only print user defined variables *) -let print (lctx : t) : unit = +let pp_print (f : Format.formatter) (lctx : t) : unit = let ranges = [(0, Myers.length lctx - !builtin_size)] in - let f = Fmt.formatter_of_out_channel stdout in Format.fprintf f "%a" (pp_print_ranges ~ranges) lctx +(** Only print user defined variables *) +let print (lctx : t) : unit = + let f = Fmt.formatter_of_out_channel stdout in + pp_print f lctx + (** Print the whole context, including builtins. *) let dump (lctx : t) : unit = let ranges = [(0, Myers.length lctx)] in ===================================== typer.ml ===================================== @@ -188,6 +188,29 @@ let dump_elexps_main argv = in () +let dump_lctx_main argv = + let usage = Sys.executable_name ^ " dump-lexps <file> …" in + parse_args ~arg_defs:dump_lexps_arg_defs argv usage; + + let dump_lexps_of_file ectx path = + let source = Source.of_path path in + let pretokens = Prelexer.prelex source in + let tokens = Lexer.lex Grammar.default_stt pretokens in + let _, ectx' = Elab.lexp_p_decls [] tokens ectx in + let f = Fmt.formatter_of_out_channel stdout in + if !print_indices then + Lexp.pp_enable_print_indices f; + Format.fprintf f "%a@." Lctx.pp_print (ectx_to_lctx ectx'); + ectx' + in + let _ = + List.fold_left + dump_lexps_of_file + Elab.default_ectx + (list_input_files ()) + in + () + let main () = let command, argv = if Array.length Sys.argv <= 1 @@ -214,6 +237,7 @@ let main () = | "dump-tokens" -> dump_tokens_main argv | "dump-lexps" -> dump_lexps_main argv | "dump-elexps" -> dump_elexps_main argv + | "dump-lctx" -> dump_lctx_main argv | _ -> eprintf {|unknown command "%s"|} command; exit 1) View it on GitLab: https://gitlab.com/monnier/typer/-/commit/023768b1d7c1c94d1ff44ee7037e3e3b0… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/023768b1d7c1c94d1ff44ee7037e3e3b0… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch gensym-without-spaces
by Simon Génier (＠ilovemonoids) 24 Mar '23

24 Mar '23

Simon Génier pushed new branch gensym-without-spaces at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/gensym-without-spaces You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][simon--pp-print-lctx] 6 commits: Move the index set to its own module.
by Simon Génier (＠ilovemonoids) 24 Mar '23

24 Mar '23

Simon Génier pushed to branch simon--pp-print-lctx at Stefan / Typer Commits: 62f468a7 by Simon Génier at 2023-03-24T16:31:56-04:00 Move the index set to its own module. I want to separate the lexp context to its own module, but it depends on the index set in Debruijn. Debruijn will depend on this new Lctx module so splitting the index set is necessary to avoid circular dependencies. - - - - - 77d866bd by Simon Génier at 2023-03-24T16:33:33-04:00 Implement IdxSet in terms of Set instead of Map. It probably ends up also using a map internally, but it makes the code more concise by not having all these () to ignore. - - - - - af3d981d by Simon Génier at 2023-03-24T16:33:38-04:00 Add a fold for IdxSet. - - - - - a49395a8 by Simon Génier at 2023-03-24T16:33:38-04:00 Move the lexp context to its own module. - - - - - 99576918 by Simon Génier at 2023-03-24T16:33:38-04:00 Merge the try and the match in Lctx.lookup. - - - - - 800d040d by Simon Génier at 2023-03-24T16:33:38-04:00 Print the lexp context with the format module. This patch introduces two important changes to the way lexp contexts are printed. - The lexp context is now formatted as a list of definitions instead of a table. This leaves more horizontal room to print the expressions themselves. For example, % index = 1, offset = 0 case_return_ : Macro; case_return_ = (__.__ (depelim) case_return_); - We leverage the recent changes to the printing of lexps to limit the size of the expressions we print. We get this for free by setting a "box" limit on the formatter. Note that this limit only applies when dumping the context: the full expression is printed when inspecting single value. Elab_arg-pos = (lambda (a : ##String) -> (lambda (b : ##String) -> (lambda … -> …))); - - - - - 16 changed files: - debug_util.ml - + src/IdxSet.ml - src/REPL.ml - src/debruijn.ml - src/elab.ml - src/eval.ml - src/fmt.ml - src/gambit.ml - src/instargs.ml - + src/lctx.ml - src/opslexp.ml - src/positivity.ml - src/unification.ml - src/util.ml - tests/instargs_test.ml - typer.ml Changes: ===================================== debug_util.ml ===================================== @@ -145,7 +145,7 @@ let main () = print_string "\n";)); (if (get_p_option "lctx") then( - print_lexp_ctx (ectx_to_lctx nctx); print_string "\n")); + Lctx.print (ectx_to_lctx nctx); print_string "\n")); (* Type erasure *) let _, clean_lxp = ===================================== src/IdxSet.ml ===================================== @@ -0,0 +1,64 @@ +(* Copyright (C) 2023 Free Software Foundation, Inc. + * + * Author: Simon Génier <simon.genier(a)umontreal.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. *) + +open Util + +(** Sets of DeBruijn indices. + + It is implemented by a set, but a global offset is stored alongside. This + makes shifting very efficient. *) +type t = db_offset * ISet.t + +let empty : t = (0, ISet.empty) + +let mem (i : db_offset) (o, m : t) : bool = + ISet.mem (i - o) m + +let set (i : db_offset) (o, m : t) : t = + (o, ISet.add (i - o) m) + +let reset (i : db_offset) (o, m : t) : t = + (o, ISet.remove (i - o) m) + +let singleton (i : db_offset) = + (0, ISet.singleton i) + +(** Adjust a set for use in a deeper scope with `o` additional bindings. *) +let sink (o : db_offset) (o', m : t) : t = + (o + o', m) + +(** Adjust a set for use in a higher scope with `o` fewer bindings. *) +let hoist (o : db_offset) (o', m : t) : t = + let newo = o' - o in + let (_, _, newm) = ISet.split (-1 - newo) m + in (newo, newm) + +let union (o1, m1 : t) (o2, m2 : t) : t = + if o1 = o2 + then (o1, ISet.union m1 m2) + else + let o = o2 - o1 in + (o1, ISet.fold (fun i2 m1 -> ISet.add (i2 + o) m1) m2 m1) + +let ascending_seq (o, m : t) : int Seq.t = + ISet.to_seq m |> Seq.map (fun x -> x + o) + +let fold (type a) (f : db_offset -> a -> a) (o, m : t) (x : a) : a = + ISet.fold (fun i x -> f (o + i) x) m x ===================================== src/REPL.ml ===================================== @@ -180,8 +180,8 @@ let rec repl i (interactive : #Backend.interactive) (ectx : elab_context) = ectx | "%info"::args | "%i"::args -> let _ = match args with - | ["all"] -> dump_lexp_ctx (ectx_to_lctx ectx) - | _ -> print_lexp_ctx (ectx_to_lctx ectx) in + | ["all"] -> Lctx.dump (ectx_to_lctx ectx) + | _ -> Lctx.print (ectx_to_lctx ectx) in ectx | cmd::_ ===================================== src/debruijn.ml ===================================== @@ -32,50 +32,13 @@ * * ---------------------------------------------------------------------------*) -open Fmt open Lexp open Sexp open Util -module M = Myers - let fatal ?print_action ?loc fmt = Log.log_fatal ~section:"DEBRUIJN" ?print_action ?loc fmt -(** Sets of DeBruijn indices **) - -type set = db_offset * unit IMap.t - -let set_empty = (0, IMap.empty) - -let set_mem i (o, m) = IMap.mem (i - o) m - -let set_set i (o, m) = (o, IMap.add (i - o) () m) -let set_reset i (o, m) = (o, IMap.remove (i - o) m) - -let set_singleton i = (0, IMap.singleton i ()) - -(* Adjust a set for use in a deeper scope with `o` additional bindings. *) -let set_sink o (o', m) = (o + o', m) - -(* Adjust a set for use in a higher scope with `o` fewer bindings. *) -let set_hoist o (o', m) = - let newo = o' - o in - let (_, _, newm) = IMap.split (-1 - newo) m - in (newo, newm) - -let set_union (o1, m1) (o2, m2) : set = - if o1 = o2 then - (o1, IMap.merge (fun _k _ _ -> Some ()) m1 m2) - else - let o = o2 - o1 in - (o1, IMap.fold (fun i2 () m1 - -> IMap.add (i2 + o) () m1) - m2 m1) - -let set_ascending_seq ((o, m) : set) : int Seq.t = - IMap.to_seq m |> Seq.map (fun x -> fst x + o) - (* Handling scoping/bindings is always tricky. So it's always important * to keep in mind for *every* expression which is its context. * @@ -159,10 +122,6 @@ let eq_refl = Anormal, mkVar (xv, 0)]))))) -(* easier to debug with type annotations *) -type env_elem = (vname * varbind * ltype) -type lexp_context = env_elem M.myers - type db_ridx = int (* DeBruijn reverse index (i.e. counting from the root). *) (* Map variable name to its distance in the context *) @@ -180,18 +139,18 @@ type typeclass_ctx = (ltype * lctx_length) list (* the list of type classes *) * bool (* true if new bindings are instances (used to implement (dont-)bind-instances) *) - * set (* The set of bindings that are instances *) + * IdxSet.t (* The set of bindings that are instances *) (* This is the *elaboration context* (i.e. a context that holds * a lexp context plus some side info. *) type elab_context - = Grammar.t * senv_type * lexp_context * meta_scope * typeclass_ctx + = Grammar.t * senv_type * Lctx.t * meta_scope * typeclass_ctx (* Elab context getters *) let get_size (ctx : elab_context) = let (_, (n, _), lctx, _, _) = ctx in - assert (n = M.length lctx); n + assert (n = Myers.length lctx); n let ectx_get_grammar (ectx : elab_context) : Grammar.t = let (grm,_, _, _, _) = ectx in grm @@ -200,7 +159,7 @@ let ectx_get_senv (ectx : elab_context) : senv_type = let (_,senv, _, _, _) = ectx in senv (* Extract the lexp context from the context used during elaboration. *) -let ectx_to_lctx (ectx : elab_context) : lexp_context = +let ectx_to_lctx (ectx : elab_context) : Lctx.t = let (_,_, lctx, _, _) = ectx in lctx let ectx_get_scope (ectx : elab_context) : meta_scope = @@ -225,7 +184,7 @@ let ectx_set_senv (senv : senv_type) (ectx : elab_context) : elab_context = let (grm, _, lctx, sl, tcctx) = ectx in (grm, senv, lctx, sl, tcctx) -let ectx_set_lctx (lctx : lexp_context) (ectx : elab_context) : elab_context = +let ectx_set_lctx (lctx : Lctx.t) (ectx : elab_context) : elab_context = let (grm, senv, _, sl, tcctx) = ectx in (grm, senv, lctx, sl, tcctx) @@ -241,11 +200,10 @@ let ectx_set_tcctx (tcctx : typeclass_ctx) (ectx : elab_context) : elab_context * ---------------------------------- *) let empty_senv = (0, SMap.empty) -let empty_lctx = M.nil -let empty_tcctx = ([], false, set_empty) +let empty_tcctx = ([], false, IdxSet.empty) let empty_elab_context : elab_context - = (Grammar.default_grammar, empty_senv, empty_lctx, + = (Grammar.default_grammar, empty_senv, Lctx.empty, (0, 0, ref SMap.empty), empty_tcctx) (* senv_lookup caller were using Not_found exception *) @@ -273,33 +231,15 @@ let senv_lookup (name: string) (ctx: elab_context): int = senv_lookup_fail (get_related_names n name map) -let lexp_ctx_cons (ctx : lexp_context) d v t = - assert (let offset = match v with | LetDef (o, _) -> o | _ -> 0 in - offset >= 0 - && (ctx = M.nil - || match M.car ctx with - | (_, LetDef (previous_offset, _), _) - -> previous_offset >= 0 (* General constraint. *) - (* Either `ctx` is self-standing (doesn't depend on us), - * or it depends on us (and maybe other bindings to come), in - * which case we have to depend on the exact same bindings. *) - && (previous_offset <= 1 - || previous_offset = 1 + offset) - | _ -> true)); - M.cons (d, v, t) ctx - -let lctx_extend (ctx : lexp_context) (def: vname) (v: varbind) (t: lexp) = - lexp_ctx_cons ctx def v t - let tcctx_extend ((tcs, inst_def, insts) : typeclass_ctx) = - let insts = set_sink 1 insts in - tcs, inst_def, if inst_def then set_set 0 insts else insts + let insts = IdxSet.sink 1 insts in + tcs, inst_def, if inst_def then IdxSet.set 0 insts else insts let tcctx_extend_rec (n : int) ((tcs, inst_def, insts) : typeclass_ctx) = let rec set_set_n n s = if n = 0 then s else - set_set_n (n - 1) (set_set (n - 1) s) in - let insts = set_sink n insts in + set_set_n (n - 1) (IdxSet.set (n - 1) s) in + let insts = IdxSet.sink n insts in tcs, inst_def, if inst_def then set_set_n n insts else insts let env_extend_rec (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = @@ -307,20 +247,11 @@ let env_extend_rec (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = let (n, map) = ectx_get_senv ctx in let nmap = match oname with None -> map | Some name -> SMap.add name n map in ctx |> ectx_set_senv (n + 1, nmap) - |> ectx_set_lctx (lexp_ctx_cons (ectx_to_lctx ctx) def v t) + |> ectx_set_lctx (Lctx.cons (ectx_to_lctx ctx) def v t) |> ectx_set_tcctx (tcctx_extend (ectx_to_tcctx ctx)) let ectx_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec ctx def v t -let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) = - let (ctx, _) = - List.fold_left - (fun (ctx, recursion_offset) (def, e, t) -> - lexp_ctx_cons ctx def (LetDef (recursion_offset, e)) t, - recursion_offset - 1) - (ctx, List.length defs) defs in - ctx - let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) = let (n, senv) = ectx_get_senv ctx in let len = List.length defs in @@ -331,7 +262,7 @@ let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) = i + 1) (senv, n) defs in ctx |> ectx_set_senv (n + len, senv') - |> ectx_set_lctx (lctx_extend_rec (ectx_to_lctx ctx) defs) + |> ectx_set_lctx (Lctx.extend (ectx_to_lctx ctx) defs) |> ectx_set_tcctx (tcctx_extend_rec len (ectx_to_tcctx ctx)) let ectx_new_scope (ectx : elab_context) : elab_context = @@ -339,12 +270,9 @@ let ectx_new_scope (ectx : elab_context) : elab_context = let (scope, _, rmmap) = ectx_get_scope ectx in ectx_set_meta_scope (scope + 1, Myers.length lctx, ref (!rmmap)) ectx -let env_lookup_by_index index (ctx: lexp_context): env_elem = +let env_lookup_by_index index (ctx: Lctx.t): Lctx.elem = Myers.nth index ctx -let env_lookup_set (s : set) (lctx : lexp_context) : (db_index * env_elem) Seq.t = - M.nthsi lctx (set_ascending_seq s) - let ectx_add_typeclass (ectx : elab_context) (t : ltype) : elab_context = let (tcs, inst_def, insts) = ectx_to_tcctx ectx in ectx_set_tcctx ((t, get_size ectx) :: tcs, inst_def, insts) ectx @@ -352,154 +280,23 @@ let ectx_add_typeclass (ectx : elab_context) (t : ltype) : elab_context = let ectx_set_inst (ectx : elab_context) (index : int) (inst : bool) : elab_context = let (tcs, inst_def, insts) = ectx_to_tcctx ectx in - let ninsts = if inst then set_set index insts else set_reset index insts in + let ninsts = if inst then IdxSet.set index insts else IdxSet.reset index insts in ectx_set_tcctx (tcs, inst_def, ninsts) ectx let ectx_set_inst_def (ectx : elab_context) (inst_def : bool) : elab_context = let (tcs, _, insts) = ectx_to_tcctx ectx in ectx_set_tcctx (tcs, inst_def, insts) ectx -let print_lexp_ctx_n (ctx : lexp_context) (ranges : (int * int) list) = - print_string (make_title " LEXP CONTEXT "); - - make_rheader - [(Some ('l', 7), "INDEX"); - (Some ('l', 4), "OFF"); - (Some ('l', 10), "NAME"); - (Some ('l', 42), "VALUE : TYPE")]; - - print_string (make_sep '-'); - - let prefix = " | | | | " in - - let print i = - try - let r, name, lexp, ty = - match env_lookup_by_index i ctx with - | ((_, name), LetDef (r, exp), ty) -> r, name, Some exp, ty - | ((_, name), _, ty) -> 0, name, None, ty - in - let name' = maybename name in - let short_name = - if String.length name' > 10 - then - String.sub name' 0 9 ^ "…" - else name' - in - Printf.printf " | %-7d | %-4d | %-10s | " i r short_name; - (match lexp with - | None -> print_string "<var>" - | Some lexp - -> (let str = Lexp.to_string lexp in - let strs = - match String.split_on_char '\n' str with - | hd :: tl -> print_string hd; tl - | [] -> [] - in - List.iter - (fun elem -> - print_newline (); - print_string prefix; - print_string elem) - strs)); - print_string " : "; - Lexp.print ty; - print_newline () - with - | Not_found - -> print_endline " | %-7d | Not_found |" - in - - let rec print_range lower i = - let i' = i - 1 in - if i' >= lower - then - (print i'; - print_range lower i') - in - - let rec print_ranges = function - | [] -> () - | (lower, upper) :: ranges' - -> (print_range lower upper; - print_ranges ranges') - in - - print_ranges ranges; - print_string (make_sep '=') - -(* Only print user defined variables *) -let print_lexp_ctx (lctx : lexp_context) : unit = - print_lexp_ctx_n lctx [(0, M.length lctx - !builtin_size)] - -(* Dump the whole context *) -let dump_lexp_ctx (lctx : lexp_context) : unit = - print_lexp_ctx_n lctx [(0, M.length lctx)] - -let summarize_lctx (lctx : lexp_context) (at : int) : unit = - let ranges = - if at < 7 - then [(0, min (max (at + 2) 5) (M.length lctx))] - else [(at - 2, min (at + 2) (M.length lctx)); (0, 5)] - in - print_lexp_ctx_n lctx ranges; - print_endline "This context was trucated. Pass the option -Vfull-lctx to view it in full." - -let log_full_lctx = ref false - -(* generic lookup *) -let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = - let ((loc, oename), dbi) = v in - try - let ret = Myers.nth dbi ctx in - let _ = match (ret, oename) with - | (((_, Some name), _, _), Some ename) - -> (* Check if names match *) - if not (ename = name) then - let print_action = - if !log_full_lctx - then fun () -> (print_lexp_ctx ctx; print_newline ()) - else fun () -> summarize_lctx ctx dbi - in - fatal - ~loc:(Sexp.location loc) ~print_action - ({|DeBruijn index %d refers to wrong name. |} - ^^ {|Expected: "%s" got "%s"|}) - dbi ename name - | _ -> () in - - ret - with - | Not_found - -> fatal - ~loc:(Sexp.location loc) - "DeBruijn index %d of `%s` out of bounds" - dbi - (maybename oename) - -let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp = - let (_, i) = vref in - let (_, _, t) = lctx_lookup ctx vref in - mkSusp t (S.shift (i + 1)) - -let lctx_lookup_value (ctx : lexp_context) (vref : vref) : lexp option = - let (_, i) = vref in - match lctx_lookup ctx vref with - | (_, LetDef (o, v), _) -> Some (push_susp v (S.shift (i + 1 - o))) - | _ -> None - let env_lookup_type ctx (v : vref): lexp = - lctx_lookup_type (ectx_to_lctx ctx) v - - (* mkSusp ltp (S.shift (idx + 1)) *) + Lctx.lookup_type (ectx_to_lctx ctx) v let env_lookup_expr ctx (v : vref): lexp option = - lctx_lookup_value (ectx_to_lctx ctx) v + Lctx.lookup_value (ectx_to_lctx ctx) v type lct_view = | CVempty - | CVlet of vname * varbind * ltype * lexp_context - | CVfix of (vname * lexp * ltype) list * lexp_context + | CVlet of vname * varbind * ltype * Lctx.t + | CVfix of (vname * lexp * ltype) list * Lctx.t let lctx_view lctx = match lctx with ===================================== src/elab.ml ===================================== @@ -164,7 +164,7 @@ let elab_check_proper_type (ctx : elab_context) ltp var = | _ -> info ~print_action:(fun _ -> - print_lexp_ctx (ectx_to_lctx ctx); print_newline () + Lctx.print (ectx_to_lctx ctx); print_newline () ) ~loc:(Lexp.location ltp) {|Exception while checking type "%s"%s|} @@ -185,7 +185,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = info ~print_action:(fun _ -> lexp_print_details lxp (); - print_lexp_ctx (ectx_to_lctx ctx); + Lctx.print (ectx_to_lctx ctx); print_newline () ) ~loc:(Sexp.location loc) @@ -276,7 +276,7 @@ let ctx_define_rec (ctx: elab_context) decls = * definitions) as well as when we fill implicit arguments. *) -let newMetavar (ctx : lexp_context) sl name t = +let newMetavar (ctx : Lctx.t) sl name t = let meta = Unif.create_metavar ctx sl t in mkMetavar (meta, S.identity, name) @@ -305,7 +305,7 @@ let newShiftedInstanceMetavar (ctx : elab_context) name t = let new_n = n - ctx_shift in (new_n, SMap.filter (fun _ n' -> n' <= new_n) senv_map) in let shift_tcctx (tcs, inst_def, insts) = - (tcs, inst_def, DB.set_hoist ctx_shift insts) in + (tcs, inst_def, IdxSet.hoist ctx_shift insts) in let nctx = ctx |> ectx_set_senv (shift_senv (ectx_get_senv ctx)) |> ectx_set_lctx octx @@ -314,10 +314,10 @@ let newShiftedInstanceMetavar (ctx : elab_context) name t = Inst.save_metavar_resolution_ctxt meta nctx (fst name); mkMetavar (meta, subst, name) -let newMetalevel (ctx : lexp_context) sl loc = +let newMetalevel (ctx : Lctx.t) sl loc = newMetavar ctx sl (loc, Some "ℓ") type_level -let newMetatype (ctx : lexp_context) sl loc +let newMetatype (ctx : Lctx.t) sl loc = newMetavar ctx sl (loc, Some "τ") (mkSort (loc, Stype (newMetalevel ctx sl loc))) ===================================== src/eval.ml ===================================== @@ -1123,27 +1123,26 @@ let eval_all lxps rctx silent = List.map (fun g -> evalfun g rctx) lxps -module CMap - (* Memoization table. FIXME: Ideally the keys should be "weak", but - * I haven't found any such functionality in OCaml's libs. *) - = Hashtbl.Make - (struct type t = lexp_context let hash = Hashtbl.hash let equal = (==) end) +(* Memoization table. FIXME: Ideally the keys should be "weak", but I haven't + found any such functionality in OCaml's libs. *) +module CMap = Hashtbl.Make(Lctx) let ctx_memo = CMap.create 1000 -let not_closed rctx ((o, vm) : DB.set) = - IMap.fold (fun i () nc -> let i = i + o in - let (_, rc) = Myers.nth i rctx in - match !rc with Vundefined -> i::nc | _ -> nc) - vm [] +let not_closed rctx (indices : IdxSet.t) : db_offset list = + let f i nc = + let (_, rc) = Myers.nth i rctx in + match !rc with Vundefined -> i::nc | _ -> nc + in + IdxSet.fold f indices [] let closed_p rctx (fvs, (mvs, _)) = not_closed rctx fvs = [] (* FIXME: Handle metavars! *) && IMap.is_empty mvs -let from_lctx (lctx: lexp_context): runtime_env = +let from_lctx (lctx : Lctx.t) : runtime_env = (* FIXME: `eval` with a disabled IO.run. *) - let rec from_lctx' (lctx: lexp_context): runtime_env = + let rec from_lctx' (lctx : Lctx.t) : runtime_env = match lctx_view lctx with | CVempty -> Myers.nil | CVlet (loname, def, _, lctx) @@ -1172,7 +1171,7 @@ let from_lctx (lctx: lexp_context): runtime_env = let _ = (* FIXME: Evaluate those defs that we can, even if not all defs * are present! *) - let lctx' = DB.lctx_extend_rec lctx defs in + let lctx' = Lctx.extend lctx defs in if alldefs && closed_p rctx (OL.fv_hoist (List.length defs) fvs) then List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx' e) nrctx) evs else () in ===================================== src/fmt.ml ===================================== @@ -118,6 +118,7 @@ let formatter_of_out_channel (chan : out_channel) : Format.formatter = print_close_stag = Fun.const (); } in - Format.pp_set_formatter_stag_functions f stag_fns; - Format.pp_set_tags f true; + pp_set_formatter_stag_functions f stag_fns; + pp_set_tags f true; + pp_set_ellipsis_text f "…"; f ===================================== src/gambit.ml ===================================== @@ -18,7 +18,6 @@ * 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 Debruijn open Elexp open Lexp open Printf @@ -136,7 +135,7 @@ module ScmContext = struct let nil : t = Myers.nil - let of_lctx (lctx : lexp_context) : t = + let of_lctx (lctx : Lctx.t) : t = let f ((_, name), _, _) = Option.get name in Myers.map f lctx ===================================== src/instargs.ml ===================================== @@ -77,7 +77,7 @@ let in_typeclass_set (ectx : DB.elab_context) (t : L.ltype) : bool = (** Get the head of a call. For instance, the call of `(Monoid α)` is `Monoid`. *) -let get_head (lctx : DB.lexp_context) (t : L.ltype) : L.ltype = +let get_head (lctx : Lctx.t) (t : L.ltype) : L.ltype = let whnft = OL.lexp_whnf t lctx in match L.lexp_lexp' whnft with | L.Call (_, head, _) -> head @@ -136,8 +136,8 @@ let search_instance return the applied expression (ex: `(nil (t := Int))` for a `(List Int)`). The expression is tupled with the index and env_elem, for convenience. *) - let env_elem_match (i, elem : U.db_index * DB.env_elem) - : (int * DB.env_elem * L.lexp) option = + let env_elem_match (i, elem : U.db_index * Lctx.elem) + : (int * Lctx.elem * L.lexp) option = let ((_, namopt), _, t') = elem in let var = L.mkVar ((sinfo, namopt), i) in let t' = L.mkSusp t' (S.shift (i + 1)) in @@ -166,7 +166,7 @@ let search_instance None | Match -> Some (i, elem, e) in - let candidates = DB.env_lookup_set insts lctx + let candidates = Lctx.lookup_set insts lctx |> Seq.filter_map env_elem_match in if !debug_list_all_candidates then ===================================== src/lctx.ml ===================================== @@ -0,0 +1,165 @@ +(* Copyright (C) 2023 Free Software Foundation, Inc. + * + * Author: Simon Génier <simon.genier(a)umontreal.ca> + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see <http://www.gnu.org/licenses/>. *) + +open Lexp +open Sexp +open Util + +let fatal ?print_action ?loc fmt = + Log.log_fatal ~section:"LCTX" ?print_action ?loc fmt + +type elem = vname * varbind * ltype + +type t = elem Myers.myers + +let empty = Myers.nil + +let cons (ctx : t) d v t = + assert (let offset = match v with | LetDef (o, _) -> o | _ -> 0 in + offset >= 0 + && (ctx = Myers.nil + || match Myers.car ctx with + | (_, LetDef (previous_offset, _), _) + -> previous_offset >= 0 (* General constraint. *) + (* Either `ctx` is self-standing (doesn't depend on us), + * or it depends on us (and maybe other bindings to come), in + * which case we have to depend on the exact same bindings. *) + && (previous_offset <= 1 + || previous_offset = 1 + offset) + | _ -> true)); + Myers.cons (d, v, t) ctx + +let extend (ctx : t) (defs: (vname * lexp * ltype) list) : t = + let (ctx, _) = + List.fold_left + (fun (ctx, recursion_offset) (def, e, t) -> + cons ctx def (LetDef (recursion_offset, e)) t, + recursion_offset - 1) + (ctx, List.length defs) defs in + ctx + +let lookup_by_index index (ctx: t) : elem = + Myers.nth index ctx + +let lookup_set (s : IdxSet.t) (lctx : t) : (db_index * elem) Seq.t = + Myers.nthsi lctx (IdxSet.ascending_seq s) + +let pp_print_elem + (f : Format.formatter) + (i : db_index) + (r : db_offset) + (name : vname) + (e : lexp option) + (ty : ltype) + : unit = + + let open Format in + let name_text = string_of_vname name in + fprintf f "%% index = @{<green>%d@}, offset = @{<green>%d@}@." i r; + fprintf f "@[<hov 2>%s :@ %a;@]@." name_text Lexp.pp_print ty; + match e with + | Some e + -> let max_boxes = pp_get_max_boxes f () in + pp_set_max_boxes f 6; + fprintf f "@[<hov 2>%s =@ %a;@]@." name_text Lexp.pp_print e; + pp_set_max_boxes f max_boxes + | None -> () + +let pp_print_ranges + (f : Format.formatter) ~(ranges : (int * int) list) (lctx : t) + : unit = + + let open Format in + let print_range (lower, upper) = + for i = upper - 1 downto lower do + match lookup_by_index i lctx with + | (name, LetDef (r, exp), ty) -> pp_print_elem f i r name (Some exp) ty + | (name, _, ty) -> pp_print_elem f i 0 name None ty + | exception Not_found -> fatal "Missing variable at index %d" i + done + in + pp_print_string f (Fmt.make_title "Lexp Context"); + List.iter print_range ranges; + pp_print_string f (Fmt.make_sep '='); + pp_print_cut f () + +(** Print a summary of the context around a given offset, plus a few of the most + recently defined variables. *) +let summarize ~(around : int) (lctx : t) : unit = + let ranges = + if around < 7 + then [(0, min (max (around + 2) 5) (Myers.length lctx))] + else [(around - 2, min (around + 2) (Myers.length lctx)); (0, 5)] + in + let f = Fmt.formatter_of_out_channel stdout in + Format.fprintf f "%a" (pp_print_ranges ~ranges) lctx; + print_endline "This context was trucated. Pass the option -Vfull-lctx to view it in full." + +(** Only print user defined variables *) +let print (lctx : t) : unit = + let ranges = [(0, Myers.length lctx - !builtin_size)] in + let f = Fmt.formatter_of_out_channel stdout in + Format.fprintf f "%a" (pp_print_ranges ~ranges) lctx + +(** Print the whole context, including builtins. *) +let dump (lctx : t) : unit = + let ranges = [(0, Myers.length lctx)] in + let f = Fmt.formatter_of_out_channel stdout in + Format.fprintf f "%a" (pp_print_ranges ~ranges) lctx + +let log_full = ref false + +(** Lookup a variable by reference. *) +let lookup (ctx : t) ((sinfo, oename), dbi : vref) : elem = + match Myers.nth dbi ctx, oename with + | exception Not_found + -> fatal + ~loc:(Sexp.location sinfo) + "DeBruijn index %d of `%s` out of bounds" + dbi + (maybename oename) + + (* Check if names match *) + | ((_, Some name), _, _), Some ename when name <> ename + -> let print_action = + if !log_full + then fun () -> print ctx + else fun () -> summarize ~around:dbi ctx + in + fatal + ~loc:(Sexp.location sinfo) ~print_action + {|DeBruijn index %d refers to wrong name. Expected "%s", but got "%s"|} + dbi ename name + + | ret, _ -> ret + +let lookup_type (ctx : t) ((_, i) as vref : vref) : lexp = + let (_, _, t) = lookup ctx vref in + mkSusp t (S.shift (i + 1)) + +let lookup_value (ctx : t) ((_, i) as vref : vref) : lexp option = + match lookup ctx vref with + | (_, LetDef (o, v), _) -> Some (push_susp v (S.shift (i + 1 - o))) + | _ -> None + +(** Two contexts are equal if they have the same identity. *) +let equal : t -> t -> bool = (==) + +let hash : t -> int = Hashtbl.hash ===================================== src/opslexp.ml ===================================== @@ -61,7 +61,7 @@ module LMap (struct type t = lexp let hash = Hashtbl.hash let equal = (==) end) let reducible_builtins - = ref (SMap.empty : (DB.lexp_context + = ref (SMap.empty : (Lctx.t -> (P.arg_kind * lexp) list (* The builtin's args *) -> lexp option) SMap.t) @@ -88,8 +88,8 @@ let impredicative_universe_poly = true (* Assume arg is TypeLevel.z when erasabl (* Lexp context *) -let lookup_type = DB.lctx_lookup_type -let lookup_value = DB.lctx_lookup_value +let lookup_type = Lctx.lookup_type +let lookup_value = Lctx.lookup_value (** Extend a substitution S with a (mutually recursive) set * of definitions DEFS. @@ -171,7 +171,7 @@ let lexp_close lctx e = the inductive type of the target (and it's typelevel). A better solution would be to add these values as annotations in the lexp datatype. *) -let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = +let rec lexp_whnf e (ctx : Lctx.t) : lexp = match lexp_lexp' e with | Var v -> (match lookup_value ctx v with | None -> e @@ -284,7 +284,7 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = | _elem -> e -and lexp'_whnf e (ctx : DB.lexp_context) : lexp' = +and lexp'_whnf e (ctx : Lctx.t) : lexp' = lexp_lexp' (lexp_whnf e ctx) and eq_cast_whnf ctx args = @@ -355,7 +355,7 @@ and level_leq (c1, m1) (c2, m2) = m1 (* Returns true if e₁ and e₂ are equal (upto alpha/beta/...). *) -and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = +and conv_p' (ctx : Lctx.t) (vs : set_plexp) e1 e2 : bool = let e1' = lexp_whnf e1 ctx in let e2' = lexp_whnf e2 ctx in e1' == e2' || @@ -384,11 +384,11 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | (Arrow (_, ak1, vd1, t11, t12), Arrow (_, ak2, _vd2, t21, t22)) -> ak1 == ak2 && conv_p t11 t21 - && conv_p' (DB.lexp_ctx_cons ctx vd1 Variable t11) (set_shift vs') + && conv_p' (Lctx.cons ctx vd1 Variable t11) (set_shift vs') t12 (srename vd1 t22) | (Lambda (ak1, l1, t1, e1), Lambda (ak2, _l2, t2, e2)) -> ak1 == ak2 && (conv_erase || conv_p t1 t2) - && conv_p' (DB.lexp_ctx_cons ctx l1 Variable t1) + && conv_p' (Lctx.cons ctx l1 Variable t1) (set_shift vs') e1 e2 | (Call (_, f1, args1), Call (_, f2, args2)) @@ -406,7 +406,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | ([], []) -> true | ((ak1,vd1,t1)::fields1, (ak2,_vd2,t2)::fields2) -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_fields (DB.lexp_ctx_cons ctx vd1 Variable t1) + && conv_fields (Lctx.cons ctx vd1 Variable t1) (set_shift vs) fields1 fields2 | _,_ -> false in @@ -418,7 +418,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = SMap.equal (conv_fields ctx vs) cases1 cases2 | ((ak1,l1,t1)::args1, (ak2,_l2,t2)::args2) -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_args (DB.lexp_ctx_cons ctx l1 Variable t1) + && conv_args (Lctx.cons ctx l1 Variable t1) (set_shift vs) args1 args2 | _,_ -> false in @@ -465,7 +465,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = (Pexp.Aerasable, tltp); (* Inductive type *) (Pexp.Anormal, hlxp); (* Lexp of the branch head *) (Pexp.Anormal, tlxp)]) in (* Target lexp *) - DB.lexp_ctx_cons ctx (dsinfo, None) Variable eqty in + Lctx.cons ctx (dsinfo, None) Variable eqty in (* The map module doesn't have a function to compare two maps with the key (which is needed to get the field types from the inductive. Instead, we work with the lists of @@ -481,7 +481,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = (ak', _vdef', ftype)::fieldtypes -> if ak1 = ak2 && ak2 = ak' then mkctx - (DB.lexp_ctx_cons ctx vdef1 Variable (mkSusp ftype s)) + (Lctx.cons ctx vdef1 Variable (mkSusp ftype s)) ((ak1, (mkVar (vdef1, i)))::args) (ssink vdef1 s) (i - 1) @@ -507,7 +507,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = ) && (match (def1, def2) with | (Some (v1, e1), Some (_v2, e2)) -> - let nctx = DB.lctx_extend ctx v1 Variable etype in + let nctx = Lctx.cons ctx v1 Variable etype in let subst = S.shift 1 in let hlxp = mkVar ((dsinfo, None), 0) in let nctx = ctx_extend_with_eq nctx subst hlxp in @@ -520,7 +520,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = subst_eq s1 s2 | (_, _) -> false -and conv_p (ctx : DB.lexp_context) e1 e2 +and conv_p (ctx : Lctx.t) e1 e2 = if e1 == e2 then true else conv_p' ctx set_empty e1 e2 @@ -582,8 +582,8 @@ and sort_compose ctx1 ctx2 l ak k1 k2 = | (_, _) -> SortK1NotType and dbset_push ak erased = - let nerased = DB.set_sink 1 erased in - if ak = P.Aerasable then DB.set_set 0 nerased else nerased + let nerased = IdxSet.sink 1 erased in + if ak = P.Aerasable then IdxSet.set 0 nerased else nerased and nerased_let defs erased = (* Let bindings are not erasable, with the important exception of @@ -593,7 +593,7 @@ and nerased_let defs erased = * to pay attention to whether the var is erasable or not. *) (* FIXME: Maybe allow more cases of erasable let-bindings. *) - let nerased = DB.set_sink (List.length defs) erased in + let nerased = IdxSet.sink (List.length defs) erased in let es = List.map (fun (_v, e, _t) -> (* Look for `x = y` where `y` is an erasable var. @@ -601,7 +601,7 @@ and nerased_let defs erased = * will be non-erasable, so in `let x = z; y = x ...` * where `z` is erasable, `x` will be found * to be erasable, but not `y`. *) - match lexp_lexp' e with Var (_, idx) -> DB.set_mem idx nerased + match lexp_lexp' e with Var (_, idx) -> IdxSet.mem idx nerased | _ -> false) defs in if not (List.mem true es) then nerased else @@ -659,11 +659,11 @@ and check'' erased ctx e = * Log.internal_error "Reached unreachable sort!"; *) DB.sort_omega) | Builtin (_, t) - -> let _ = check_type DB.set_empty Myers.nil t in + -> let _ = check_type IdxSet.empty Myers.nil t in t (* FIXME: Check recursive references. *) | Var (((loc, name), idx) as v) - -> if DB.set_mem idx erased then + -> if IdxSet.mem idx erased then log_tc_error ~loc:(Sexp.location loc) {|Var `%s` can't be used here, because it's erasable|} @@ -673,17 +673,17 @@ and check'' erased ctx e = | Let (l, defs, e) -> let _ = List.fold_left (fun ctx (v, _e, t) - -> (let _ = check_type DB.set_empty ctx t in - DB.lctx_extend ctx v ForwardRef t)) + -> (let _ = check_type IdxSet.empty ctx t in + Lctx.cons ctx v ForwardRef t)) ctx defs in let nerased = nerased_let defs erased in - let nctx = DB.lctx_extend_rec ctx defs in + let nctx = Lctx.extend ctx defs in (* FIXME: Termination checking! Positivity-checker! *) let _ = List.fold_left (fun n (_v, e, t) -> assert_type nctx e - (check (if DB.set_mem (n - 1) nerased - then DB.set_empty + (check (if IdxSet.mem (n - 1) nerased + then IdxSet.empty else nerased) nctx e) (push_susp t (S.shift n)); @@ -693,8 +693,8 @@ and check'' erased ctx e = (lexp_defs_subst l S.identity defs) | Arrow (loc, ak, v, t1, t2) -> (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 + let nctx = Lctx.cons ctx v Variable t1 in + let k2 = check_type (IdxSet.sink 1 erased) nctx t2 in match sort_compose ctx nctx loc ak k1 k2 with | SortResult k -> k | SortInvalid @@ -707,16 +707,16 @@ and check'' erased ctx e = -> log_tc_error ~loc:(Lexp.location t2) "Not a proper type"; mkSort (loc, StypeOmega)) | Lambda (ak, ((l,_) as v), t, e) - -> (let _k = check_type DB.set_empty ctx t in + -> (let _k = check_type IdxSet.empty ctx t in mkArrow (l, ak, v, t, check (dbset_push ak erased) - (DB.lctx_extend ctx v Variable t) + (Lctx.cons ctx v Variable t) e)) | Call (_, f, args) -> let ft = check erased ctx f in List.fold_left (fun ft (ak,arg) - -> let at = check (if ak = P.Aerasable then DB.set_empty else erased) + -> let at = check (if ak = P.Aerasable then IdxSet.empty else erased) ctx arg in match lexp'_whnf ft ctx with | Arrow (_l, ak', _v, t1, t2) @@ -761,12 +761,12 @@ and check'' erased ctx e = -> log_tc_error ~loc:(Lexp.location t) ~print_action:(fun _ -> - DB.print_lexp_ctx ictx; print_newline ()) + Lctx.print ictx; print_newline ()) "Field type %s is not a Type! (%s)" (Lexp.to_string t) (Lexp.to_string lwhnf); level), - DB.lctx_extend ictx v Variable t, - DB.set_sink 1 erased, + Lctx.cons ictx v Variable t, + IdxSet.sink 1 erased, (* The final type(level) cannot refer * to the fields! *) S.cons @@ -781,9 +781,9 @@ and check'' erased ctx e = cases (mkSortLevel SLz) in mkSort (l, Stype level) | (ak, v, t)::args - -> let _k = check_type DB.set_empty ctx t in + -> let _k = check_type IdxSet.empty ctx t in mkArrow (lexp_sinfo t, ak, v, t, - arg_loop (DB.lctx_extend ctx v Variable t) + arg_loop (Lctx.cons ctx v Variable t) (dbset_push ak erased) args) in let tct = arg_loop ctx erased args in @@ -872,7 +872,7 @@ and check'' erased ctx e = (Pexp.Anormal, tlxp)]) in (* Target lexp *) (* The eq proof is erasable. *) let nerased = dbset_push Pexp.Aerasable nerased in - let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in + let nctx = Lctx.cons ctx (l, None) Variable eqty in (nerased, nctx) in SMap.iter (fun name (l, vdefs, branch) @@ -884,7 +884,7 @@ and check'' erased ctx e = * appears in type annotations. *) | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes -> mkctx (dbset_push ak erased) - (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) + (Lctx.cons ctx vdef Variable (mkSusp ftype s)) (ssink vdef s) (mkCall (l, mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) vdefs fieldtypes @@ -907,8 +907,8 @@ and check'' erased ctx e = | Some (v, d) -> if diff <= 0 then log_tc_warning ~loc:(Sexp.location l) "Redundant default clause"; - let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in - let nerased = DB.set_sink 1 erased in + let nctx = (Lctx.cons ctx v (LetDef (0, e)) etype) in + let nerased = IdxSet.sink 1 erased in let subst = S.shift 1 in let hlxp = mkVar ((l, None), 0) in let (nerased, nctx) = @@ -962,7 +962,7 @@ and check'' erased ctx e = | MVar (_, t, _) -> push_susp t s) and check' ctx e = - let res = check'' DB.set_empty ctx e in + let res = check'' IdxSet.empty ctx e in (Log.stop_on_error (); res) and check ctx e = check' ctx e @@ -995,14 +995,14 @@ and mv_set_erase (ms, _nes) = (ms, IMap.empty) and fv_memo = LMap.create 1000 -and fv_empty = (DB.set_empty, mv_set_empty) +and fv_empty = (IdxSet.empty, mv_set_empty) and fv_union (fv1, mv1) (fv2, mv2) - = (DB.set_union fv1 fv2, mv_set_union mv1 mv2) -and fv_sink n (fvs, mvs) = (DB.set_sink n fvs, mvs) -and fv_hoist n (fvs, mvs) = (DB.set_hoist n fvs, mvs) + = (IdxSet.union fv1 fv2, mv_set_union mv1 mv2) +and fv_sink n (fvs, mvs) = (IdxSet.sink n fvs, mvs) +and fv_hoist n (fvs, mvs) = (IdxSet.hoist n fvs, mvs) and fv_erase (fvs, mvs) = (fvs, mv_set_erase mvs) -and fv (e : lexp) : (DB.set * mv_set) = +and fv (e : lexp) : IdxSet.t * mv_set = let fv' e = match lexp_lexp' e with | Imm _ -> fv_empty | SortLevel SLz -> fv_empty @@ -1011,7 +1011,7 @@ and fv (e : lexp) : (DB.set * mv_set) = | Sort (_, Stype e) -> fv e | Sort (_, (StypeOmega | StypeLevel)) -> fv_empty | Builtin _ -> fv_empty - | Var (_, i) -> (DB.set_singleton i, mv_set_empty) + | Var (_, i) -> (IdxSet.singleton i, mv_set_empty) | Proj (_, lxp, _) -> fv lxp | Susp (e, s) -> fv (push_susp e s) | Let (_, defs, e) @@ -1151,19 +1151,19 @@ and get_type ctx e = etype) | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) - -> let nctx = DB.lctx_extend_rec ctx defs in + -> let nctx = Lctx.extend ctx defs in mkSusp (get_type nctx e) (lexp_defs_subst l S.identity defs) | Arrow (l, ak, v, t1, t2) (* FIXME: Use `check` here but silencing errors? *) -> (let k1 = get_type ctx t1 in - let nctx = DB.lexp_ctx_cons ctx v Variable t1 in + let nctx = Lctx.cons ctx v Variable t1 in let k2 = get_type nctx t2 in match sort_compose ctx nctx l ak k1 k2 with | SortResult k -> k | _ -> mkSort (l, StypeOmega)) | Lambda (ak, ((l,_) as v), t, e) -> (mkArrow (l, ak, v, t, - get_type (DB.lctx_extend ctx v Variable t) + get_type (Lctx.cons ctx v Variable t) e)) | Call (_l, f, args) -> let ft = get_type ctx f in @@ -1194,7 +1194,7 @@ and get_type ctx e = -> mkSLlub ctx level (mkSusp level' subst) | _tt -> level), - DB.lctx_extend ictx v Variable t, + Lctx.cons ictx v Variable t, (* The final type(level) cannot refer * to the fields! *) S.cons @@ -1209,7 +1209,7 @@ and get_type ctx e = mkSort (l, Stype level) | (ak, v, t)::args -> mkArrow (lexp_sinfo t, ak, v, t, - arg_loop args (DB.lctx_extend ctx v Variable t)) in + arg_loop args (Lctx.cons ctx v Variable t)) in let tct = arg_loop args ctx in tct | Case (_l, _e, ret, _branches, _default) -> ret @@ -1258,7 +1258,7 @@ let _ = register_reducible_builtins () let erasure_dummy = DB.type0 let arity_of_cons - (lctx : DB.lexp_context) + (lctx : Lctx.t) (ty : lexp) (location, name : symbol) : int = @@ -1319,7 +1319,7 @@ let pos_of_label lctx label e : int = 0 -let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = +let rec erase_type (lctx : Lctx.t) (lxp: lexp) : E.elexp = match lexp_lexp' lxp with | L.Imm (s) -> E.Imm (s) | L.Builtin (v, _) -> E.Builtin (v) @@ -1333,7 +1333,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = -> erase_type lctx (L.push_susp body (S.substitute erasure_dummy)) | L.Lambda (_, vdef, ty, body) - -> let lctx' = DB.lctx_extend lctx vdef Variable ty in + -> let lctx' = Lctx.cons lctx vdef Variable ty in E.Lambda (vdef, erase_type lctx' body) | L.Let (l, decls, body) @@ -1367,10 +1367,10 @@ and clean_arg lctx = function | (_, lexp) -> Some (erase_type lctx lexp) and clean_decls - (lctx : DB.lexp_context) + (lctx : Lctx.t) (decls : ldecl list) - : DB.lexp_context * (vname * E.elexp) list = - let lctx' = DB.lctx_extend_rec lctx decls in + : Lctx.t * (vname * E.elexp) list = + let lctx' = Lctx.extend lctx decls in (lctx', List.map (fun (v, lexp, _) -> (v, erase_type lctx' lexp)) decls) and clean_default lctx lxp = @@ -1389,7 +1389,7 @@ and clean_branch_map lctx cases = clean_arg_list tl acc (S.cons erasure_dummy subst) lctx | (_, var) :: tl -> (* Keep the variable and sink the substitution. *) - let lctx' = DB.lctx_extend lctx var Variable erasure_dummy in + let lctx' = Lctx.cons lctx var Variable erasure_dummy in clean_arg_list tl (var :: acc) (ssink var subst) lctx' | [] -> (List.rev acc, subst, lctx) in @@ -1418,11 +1418,11 @@ let erase_type lctx lxp = (* Textually identical to the previous definition of `clean_decls`, but calls the new `erase_type`, which checks for metavars. *) let clean_decls - (lctx : DB.lexp_context) + (lctx : Lctx.t) (decls : ldecl list) - : DB.lexp_context * (vname * E.elexp) list = + : Lctx.t * (vname * E.elexp) list = - let lctx' = DB.lctx_extend_rec lctx decls in + let lctx' = Lctx.extend lctx decls in (lctx', List.map (fun (v, lexp, _) -> (v, erase_type lctx' lexp)) decls) (** Turning a set of declarations into an object. **) ===================================== src/positivity.ml ===================================== @@ -50,7 +50,7 @@ open Util (* Computes if the judgement x ∉ fv(τ) holds. *) let absent index lexp = let fv, _ = Opslexp.fv lexp in - not (Debruijn.set_mem index fv) + not (IdxSet.mem index fv) let rec absent_in_bindings index bindings = match bindings with ===================================== src/unification.ml ===================================== @@ -37,7 +37,7 @@ let create_metavar_1 (sl : scope_level) (t : ltype) (clen : int) (!metavar_table); idx -let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype) +let create_metavar (ctx : Lctx.t) (sl : scope_level) (t : ltype) = create_metavar_1 sl t (Myers.length ctx) let dloc = DB.dloc @@ -50,7 +50,7 @@ type constraint_kind = (* FIXME: Each constraint should additionally come with a description of how it relates to its "top-level" or some other info which might let us fix the problem (e.g. by introducing coercions). *) -type constraints = (constraint_kind * DB.lexp_context * lexp * lexp) list +type constraints = (constraint_kind * Lctx.t * lexp * lexp) list type return_type = constraints @@ -215,12 +215,12 @@ let matching_instantiation_check *) let rec unify ?(matching : scope_level option) (e1: lexp) (e2: lexp) - (ctx : DB.lexp_context) + (ctx : Lctx.t) : return_type = unify' e1 e2 ctx OL.set_empty matching and unify' (e1: lexp) (e2: lexp) - (ctx : DB.lexp_context) (vs : OL.set_plexp) + (ctx : Lctx.t) (vs : OL.set_plexp) (msl : scope_level option) (* matching mode optional scope level *) : return_type = if e1 == e2 then [] else @@ -290,7 +290,7 @@ and unify_arrow (matching : scope_level option) (arrow: lexp) (lxp: lexp) ctx vs -> if var_kind1 = var_kind2 then (unify' ltype1 ltype2 ctx vs matching) @(unify' lexp1 (srename v1 lexp2) - (DB.lexp_ctx_cons ctx v1 Variable ltype1) + (Lctx.cons ctx v1 Variable ltype1) (OL.set_shift vs) matching) else [(CKimpossible, ctx, arrow, lxp)] | (_, _) -> [(CKimpossible, ctx, arrow, lxp)] @@ -308,7 +308,7 @@ and unify_lambda (matching : scope_level option) -> if var_kind1 = var_kind2 then (unify' ltype1 ltype2 ctx vs matching) @(unify' lexp1 lexp2 - (DB.lexp_ctx_cons ctx v1 Variable ltype1) + (Lctx.cons ctx v1 Variable ltype1) (OL.set_shift vs) matching) else [(CKimpossible, ctx, lambda, lxp)] | (_, _) -> [(CKimpossible, ctx, lambda, lxp)] @@ -626,7 +626,7 @@ and unify_inductive' (matching : scope_level option) ctx vs (ctx, vs, [(CKimpossible, ctx, e1, e2)]) else List.fold_left (fun (ctx, vs, residue) ((ak1, v1, t1), (ak2, _v2, t2)) - -> (DB.lexp_ctx_cons ctx v1 Variable t1, + -> (Lctx.cons ctx v1 Variable t1, OL.set_shift vs, if not (ak1 == ak2) then [(CKimpossible, ctx, e1, e2)] else (unify' t1 t2 ctx vs matching) @ residue)) ===================================== src/util.ml ===================================== @@ -22,6 +22,7 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) module SMap = Map.Make(String) module IMap = Map.Make(Int) +module ISet = Set.Make(Int) type location = Source.Location.t let dummy_location = Source.Location.dummy ===================================== tests/instargs_test.ml ===================================== @@ -88,7 +88,7 @@ instance d; match L.lexp_lexp' (lexp_from_str lstr ctx) with | L.Var (_,idx) -> add_test ("is `" ^ lstr ^ "` an instance ?") (fun _ -> - expect_equal_bool (DB.set_mem idx insts) b + expect_equal_bool (IdxSet.mem idx insts) b ) | _ -> failwith "Impossible" ) [("a", true); ("b", false); ("c", false); ("d", true)]) ===================================== typer.ml ===================================== @@ -39,7 +39,7 @@ let arg_defs = ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity"); ("-Vfull-lctx", - Arg.Set Debruijn.log_full_lctx, + Arg.Set Lctx.log_full, "Print the full lexp context on error"); ("-Vmacro-expansion", View it on GitLab: https://gitlab.com/monnier/typer/-/compare/54bdd38af3aad1ebc85ebcd709792aa6… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/54bdd38af3aad1ebc85ebcd709792aa6… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][simon--pp-print-lctx] 13 commits: Fix an inf-loop during elaboration
by Simon Génier (＠ilovemonoids) 24 Mar '23

24 Mar '23

Simon Génier pushed to branch simon--pp-print-lctx at Stefan / Typer Commits: 4421b8e7 by Stefan Monnier at 2023-03-21T23:25:52-04:00 Fix an inf-loop during elaboration When `typer-identifier` is redefined as something else than a special form or a macro, we got into an inf-loop when elaborating X because we would rewrite to (typer_identifier X), which would then be taken as a function call, which recursively elaborates its arg X, ... * src/elab.ml (sform_immediate, sform_identifier): Move before `elaborate`. (elab_via): New function. (elaborate): Use it. - - - - - 22282068 by Simon Génier at 2023-03-22T18:03:27-04:00 Merge branch 'simon--source-container' - - - - - e13d2142 by Simon Génier at 2023-03-22T18:05:48-04:00 Use format to print pretokens. - - - - - e350b2d7 by Simon Génier at 2023-03-22T18:10:14-04:00 Use Format to print sexps. - - - - - 08503fe0 by Simon Génier at 2023-03-22T18:10:18-04:00 Use Format to print lexps. - - - - - 9f89fdce by Simon Génier at 2023-03-22T18:10:18-04:00 Use Format to print elexps. - - - - - 2c710bed by Simon Génier at 2023-03-24T16:23:32-04:00 Merge remote-tracking branch 'origin/simon--pp-print' - - - - - 52c8fa7e by Simon Génier at 2023-03-24T16:26:13-04:00 Move the index set to its own module. I want to separate the lexp context to its own module, but it depends on the index set in Debruijn. Debruijn will depend on this new Lctx module so splitting the index set is necessary to avoid circular dependencies. - - - - - 7751fa1f by Simon Génier at 2023-03-24T16:26:14-04:00 Implement IdxSet in terms of Set instead of Map. It probably ends up also using a map internally, but it makes the code more concise by not having all these () to ignore. - - - - - 399b98e3 by Simon Génier at 2023-03-24T16:26:14-04:00 Add a fold for IdxSet. - - - - - 734e0278 by Simon Génier at 2023-03-24T16:26:14-04:00 Move the lexp context to its own module. - - - - - 53e2324b by Simon Génier at 2023-03-24T16:26:14-04:00 Merge the try and the match in Lctx.lookup. - - - - - 54bdd38a by Simon Génier at 2023-03-24T16:26:14-04:00 Print the lexp context with the format module. This patch introduces two important changes to the way lexp contexts are printed. - The lexp context is now formatted as a list of definitions instead of a table. This leaves more horizontal room to print the expressions themselves. For example, % index = 1, offset = 0 case_return_ : Macro; case_return_ = (__.__ (depelim) case_return_); - We leverage the recent changes to the printing of lexps to limit the size of the expressions we print. We get this for free by setting a "box" limit on the formatter. Note that this limit only applies when dumping the context: the full expression is printed when inspecting single value. Elab_arg-pos = (lambda (a : ##String) -> (lambda (b : ##String) -> (lambda … -> …))); - - - - - 18 changed files: - − .idea/workspace.xml - debug_util.ml - + src/IdxSet.ml - src/REPL.ml - src/debruijn.ml - − src/debug.ml - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/gambit.ml - src/instargs.ml - src/inverse_subst.ml - + src/lctx.ml - src/lexer.ml - src/lexp.ml - src/listx.ml → src/list.ml The diff was not included because it is too large. View it on GitLab: https://gitlab.com/monnier/typer/-/compare/f378c4e86ab88aa7a2ccd8201299fe9a… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/f378c4e86ab88aa7a2ccd8201299fe9a… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch simon--pp-print
by Simon Génier (＠ilovemonoids) 24 Mar '23

24 Mar '23

Simon Génier deleted branch simon--pp-print at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][main] 5 commits: Use format to print pretokens.
by Simon Génier (＠ilovemonoids) 24 Mar '23

24 Mar '23

Simon Génier pushed to branch main at Stefan / Typer Commits: e13d2142 by Simon Génier at 2023-03-22T18:05:48-04:00 Use format to print pretokens. - - - - - e350b2d7 by Simon Génier at 2023-03-22T18:10:14-04:00 Use Format to print sexps. - - - - - 08503fe0 by Simon Génier at 2023-03-22T18:10:18-04:00 Use Format to print lexps. - - - - - 9f89fdce by Simon Génier at 2023-03-22T18:10:18-04:00 Use Format to print elexps. - - - - - 2c710bed by Simon Génier at 2023-03-24T16:23:32-04:00 Merge remote-tracking branch 'origin/simon--pp-print' - - - - - 28 changed files: - − .idea/workspace.xml - debug_util.ml - src/debruijn.ml - − src/debug.ml - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/gambit.ml - src/instargs.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml - src/listx.ml → src/list.ml - src/opslexp.ml - src/pexp.ml - src/prelexer.ml - src/sexp.ml - src/source.ml - src/unification.ml - src/util.ml - tests/instargs_test.ml - tests/lexer_test.ml - tests/positivity_test.ml - tests/unify_test.ml - tests/utest_lib.ml - typer.ml Changes: ===================================== .idea/workspace.xml deleted ===================================== @@ -1,41 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<project version="4"> - <component name="ChangeListManager"> - <list default="true" id="41ac7a90-abda-4ce7-87d2-87842cc79039" name="Changes" comment="" /> - <option name="SHOW_DIALOG" value="false" /> - <option name="HIGHLIGHT_CONFLICTS" value="true" /> - <option name="HIGHLIGHT_NON_ACTIVE_CHANGELIST" value="false" /> - <option name="LAST_RESOLUTION" value="IGNORE" /> - </component> - <component name="Git.Settings"> - <option name="RECENT_GIT_ROOT_PATH" value="$PROJECT_DIR$" /> - </component> - <component name="MarkdownSettingsMigration"> - <option name="stateVersion" value="1" /> - </component> - <component name="ProjectId" id="29qQStX1boOkZ1Gb6bTR6iBqd5o" /> - <component name="ProjectLevelVcsManager" settingsEditedManually="true"> - <ConfirmationsSetting value="2" id="Add" /> - </component> - <component name="ProjectViewState"> - <option name="hideEmptyMiddlePackages" value="true" /> - <option name="showLibraryContents" value="true" /> - </component> - <component name="PropertiesComponent">{ - "keyToString": { - "RunOnceActivity.OpenProjectViewOnStart": "true", - "RunOnceActivity.ShowReadmeOnStart": "true" - } -}</component> - <component name="SpellCheckerSettings" RuntimeDictionaries="0" Folders="0" CustomDictionaries="0" DefaultDictionary="application-level" UseSingleDictionary="true" transferred="true" /> - <component name="TaskManager"> - <task active="true" id="Default" summary="Default task"> - <changelist id="41ac7a90-abda-4ce7-87d2-87842cc79039" name="Changes" comment="" /> - <created>1653838146676</created> - <option name="number" value="Default" /> - <option name="presentableId" value="Default" /> - <updated>1653838146676</updated> - </task> - <servers /> - </component> -</project> \ No newline at end of file ===================================== debug_util.ml ===================================== @@ -32,38 +32,24 @@ open Typerlib -open Printf - (* Utilities *) -open Util open Fmt -open Debug (* ASTs *) -open Sexp open Lexp (* AST reader *) open Prelexer open Lexer open Eval -module EL = Elexp -module OL = Opslexp (* definitions *) open Grammar -open Builtin (* environments *) open Debruijn open Env -let dloc = dummy_location -let dsinfo = DB.dsinfo -let dummy_decl = Imm(String(dloc, "Dummy")) - -let discard _v = () - (* Argument parsing *) let arg_print_options = ref SMap.empty let arg_files = ref [] @@ -79,83 +65,17 @@ let get_p_option name = with Not_found -> false -(* - pretty ? (print with new lines and indents) - indent level - print_type? (print inferred Type) - print_index (print dbi index) - separate decl (print extra newline between declarations) - indent size 4 - highlight (use console color to display hints) -*) - -let format_mode = ref false -let ppctx = ref pretty_ppctx -let format_dest = ref "" -let write_file = ref false - -let mod_ctx name v = let f ctx = ctx := SMap.add name v !ctx in - f ppctx; f debug_ppctx - -let set_print_type v () = mod_ctx "print_type" (Bool v) -let set_print_index v () = mod_ctx "print_dbi" (Bool v) -let set_print_indent_size v = mod_ctx "indent_size" (Int v) -let set_highlight v () = mod_ctx "color" (Bool v) -let set_print_pretty v () = mod_ctx "pretty" (Bool v) - -let output_to_file str = - write_file := true; - format_dest := str; - set_highlight false () - - let arg_defs = [ - (* format *) - ("--format", - Arg.Unit (fun () -> format_mode := true), " format a typer source code"); - ("-fmt-type=on", - Arg.Unit (set_print_type true), " Print type info"); - ("-fmt-pretty=on", - Arg.Unit (set_print_pretty true), " Print with indentation"); - ("-fmt-pretty=off", - Arg.Unit (set_print_pretty false), " Print expression in one line"); - ("-fmt-type=off", - Arg.Unit (set_print_type false), " Don't print type info"); - ("-fmt-index=on", - Arg.Unit (set_print_index true), " Print DBI index"); - ("-fmt-index=off", - Arg.Unit (set_print_index false), " Don't print DBI index"); - ("-fmt-indent-size", - Arg.Int set_print_indent_size, " Indent size"); - ("-fmt-highlight=on", - Arg.Unit (set_highlight true), " Enable Highlighting for typer code"); - ("-fmt-highlight=off", - Arg.Unit (set_highlight false), " Disable Highlighting for typer code"); - ("-fmt-file", - Arg.String output_to_file, " Output formatted code to a file"); - ("-typecheck", Arg.Unit (add_p_option "typecheck"), " Enable type checking"); (* Debug *) - ("-pretok", - Arg.Unit (add_p_option "pretok"), " Print pretok debug info"); - ("-tok", - Arg.Unit (add_p_option "tok"), " Print tok debug info"); - ("-pexp", - Arg.Unit (add_p_option "pexp"), " Print pexp debug info"); - ("-lexp", - Arg.Unit (add_p_option "lexp"), " Print lexp debug info"); ("-lctx", Arg.Unit (add_p_option "lctx"), " Print lexp context"); ("-rctx", Arg.Unit (add_p_option "rctx"), " Print runtime context"); ("-all", Arg.Unit (fun () -> - add_p_option "pretok" (); - add_p_option "tok" (); - add_p_option "pexp" (); - add_p_option "lexp" (); add_p_option "lctx" (); add_p_option "rctx" ();), " Print all debug info"); @@ -166,35 +86,7 @@ let parse_args () = let make_default () = arg_print_options := SMap.empty; - add_p_option "pexp" (); - add_p_option "lexp" () - - -let format_source () = - print_string (make_title " ERRORS "); - - let filename = List.hd (!arg_files) in - let source = Source.of_path filename in - let pretoks = prelex source in - let toks = lex default_stt pretoks in - let ctx = Elab.default_ectx in - let lexps, _ = Elab.lexp_p_decls [] toks ctx in - - print_string (make_sep '-'); print_string "\n"; - - let result = lexp_str_decls (!ppctx) (List.flatten lexps) in - - if (!write_file) then ( - print_string (" " ^ " Writing output file: " ^ (!format_dest) ^ "\n"); - let file = open_out (!format_dest) in - - List.iter (fun str -> output_string file str) result; - - flush_all (); - close_out file; - - ) else (List.iter (fun str -> - print_string str; print_string "\n") result;) + add_p_option "lctx" () let main () = parse_args (); @@ -208,9 +100,6 @@ let main () = if arg_n == 1 then (Arg.usage (Arg.align arg_defs) usage) - else if (!format_mode) then ( - format_source () - ) else( (if (!debug_arg) = 0 then make_default ()); @@ -222,19 +111,11 @@ let main () = let pretoks = prelex source in print_string reset; - (if (get_p_option "pretok") then( - print_string (make_title " PreTokens"); - debug_pretokens_print_all pretoks; print_string "\n")); - (* get sexp/tokens *) print_string yellow; let toks = lex default_stt pretoks in print_string reset; - (if (get_p_option "tok") then( - print_string (make_title " Base Sexp"); - debug_sexp_print_all toks; print_string "\n")); - (* get lexp *) let octx = Elab.default_ectx in @@ -250,16 +131,6 @@ let main () = let ctx = nctx in let flexps = List.flatten lexps in - (if (get_p_option "lexp-merge-debug") then( - List.iter (fun ((_l, s), lxp, ltp) -> - printf "%-20s" (maybename s); - lexp_print ltp; print_string "\n"; - - printf "%-20s" (maybename s); - lexp_print lxp; print_string "\n"; - - ) flexps)); - (* get typecheck context *) (if (get_p_option "typecheck") then( print_string (make_title " TYPECHECK "); @@ -273,10 +144,6 @@ let main () = print_string (" " ^ (make_line '-' 76)); print_string "\n";)); - (if (get_p_option "lexp") then( - print_string (make_title " Lexp "); - debug_lexp_decls flexps; print_string "\n")); - (if (get_p_option "lctx") then( print_lexp_ctx (ectx_to_lctx nctx); print_string "\n")); ===================================== src/debruijn.ml ===================================== @@ -32,18 +32,12 @@ * * ---------------------------------------------------------------------------*) -module Str = Str - -open Util - -open Sexp - +open Fmt open Lexp +open Sexp +open Util module M = Myers -open Fmt - -module S = Subst let fatal ?print_action ?loc fmt = Log.log_fatal ~section:"DEBRUIJN" ?print_action ?loc fmt @@ -396,7 +390,7 @@ let print_lexp_ctx_n (ctx : lexp_context) (ranges : (int * int) list) = (match lexp with | None -> print_string "<var>" | Some lexp - -> (let str = lexp_str (!debug_ppctx) lexp in + -> (let str = Lexp.to_string lexp in let strs = match String.split_on_char '\n' str with | hd :: tl -> print_string hd; tl @@ -409,7 +403,7 @@ let print_lexp_ctx_n (ctx : lexp_context) (ranges : (int * int) list) = print_string elem) strs)); print_string " : "; - lexp_print ty; + Lexp.print ty; print_newline () with | Not_found @@ -468,7 +462,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = else fun () -> summarize_lctx ctx dbi in fatal - ~loc:(sexp_location loc) ~print_action + ~loc:(Sexp.location loc) ~print_action ({|DeBruijn index %d refers to wrong name. |} ^^ {|Expected: "%s" got "%s"|}) dbi ename name @@ -478,7 +472,10 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = with | Not_found -> fatal - ~loc:(sexp_location loc) "DeBruijn index %d of `%s` out of bounds" dbi (maybename oename) + ~loc:(Sexp.location loc) + "DeBruijn index %d of `%s` out of bounds" + dbi + (maybename oename) let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp = let (_, i) = vref in ===================================== src/debug.ml deleted ===================================== @@ -1,151 +0,0 @@ -(* - * Typer Compiler - * - * --------------------------------------------------------------------------- - * - * Copyright (C) 2011-2020 Free Software Foundation, Inc. - * - * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> - * Keywords: languages, lisp, dependent types. - * - * This file is part of Typer. - * - * Typer is free software; you can redistribute it and/or modify it under the - * terms of the GNU General Public License as published by the Free Software - * Foundation, either version 3 of the License, or (at your option) any - * later version. - * - * Typer is distributed in the hope that it will be useful, but WITHOUT ANY - * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS - * FOR A PARTICULAR PURPOSE. See the GNU General Public License for - * more details. - * - * You should have received a copy of the GNU General Public License along - * with this program. If not, see <http://www.gnu.org/licenses/>. - * - * --------------------------------------------------------------------------- - * - * Description: - * Provide helper functions to print out extracted - * Pretoken, Sexp, pexp and lexp - * - * --------------------------------------------------------------------------- *) - -open Printf - -(* removes some warnings *) -open Util -open Fmt - -open Prelexer - -open Sexp -open Lexp - -let print_info (message : string) (location : Source.Location.t) : unit = - Printf.printf "%s[%s]" message (Source.Location.to_string location) - -(* Print aPretokens *) -let debug_pretokens_print pretoken = - print_string " "; - - match pretoken with - | Preblock (loc, pts) - -> print_info "Preblock: " loc; - print_string "{"; - pretokens_print pts; - print_string " }" - - | Pretoken (loc, str) - -> print_info "Pretoken: " loc; - print_string ("'" ^ str ^ "'"); - - | Prestring (loc, str) - -> print_info "Prestring: " loc; - print_string ("\"" ^ str ^ "\"") - -(* Print a List of Pretokens *) -let debug_pretokens_print_all pretokens = - List.iter (fun pt -> debug_pretokens_print pt; print_string "\n") pretokens - -(* Sexp Print *) -let debug_sexp_print sexp = - match sexp with - | Symbol(_, "") - -> print_string "Epsilon " (* "ε" *) - - | Block(loc, pts) - -> print_info "Block: " loc; - print_string "{"; pretokens_print pts; print_string " }" - - | Symbol(loc, name) - -> print_info "Symbol: " loc; print_string name - - | String(loc, str) - -> print_info "String: " loc; - print_string "\""; print_string str; print_string "\"" - - | Integer(loc, n) - -> print_info "Integer: " loc; Z.print n - - | Float(loc, x) - -> print_info "Float: " loc; print_float x - - | Node(location, f, args) - -> print_info "Node: " location; - sexp_print f; print_string " ["; - List.iter (fun sexp -> print_string " "; sexp_print sexp) - args; - print_string "]" - -(* Print a list of sexp *) -let debug_sexp_print_all tokens = - List.iter (fun pt -> - print_string " "; - debug_sexp_print pt; - print_string "\n";) - tokens - - -(* Print a Pexp with debug info *) -let debug_pexp_print ptop = - print_string " "; - let l = sexp_location ptop in - let print_info msg loc pex = - print_info msg loc; - sexp_print pex in - print_info (sexp_name ptop) l ptop - -let debug_lexp_decls decls = - let sep = " : " in - List.iter (fun e -> - let ((sinfo, _name), lxp, _ltp) = e in - let loc = sexp_location sinfo in - - printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string loc); - - let str = lexp_str_decls (!debug_ppctx) [e] in - - (* First col size = 15 + 1 + 2 + 3 + 5 + 6 - * = 32 *) - - let str = match str with - | fst::tl -> print_string (sep ^ fst); print_string "\n"; tl - | _ -> [] in - - (* inefficient but makes things pretty iff -fmt-pretty=on *) - let str = List.flatten (List.map (fun g -> str_split g '\n') str) in - - let str = match str with - | scd :: tl - -> let file = Source.Container.name loc.container in - printf " FILE: %-25s : %s\n" file scd; - tl - | _ -> [] in - - List.iter (fun g -> - print_string ((make_line ' ' 32) ^ sep); - print_string g; print_string "\n") - str; - - ) decls ===================================== src/elab.ml ===================================== @@ -88,7 +88,7 @@ let print_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 + print_indent_line (Lexp.to_string lexp) let value_print_details value () = print_details value_name value_string value @@ -145,17 +145,17 @@ let sform_default_ectx = ref empty_elab_context let elab_check_sort (ctx : elab_context) lsort (var: vname) ltp = match (try OL.lexp'_whnf lsort (ectx_to_lctx ctx) with e -> - info ~print_action:(fun _ -> lexp_print lsort; print_newline ()) - ~loc:(lexp_location lsort) + 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 tystr = lexp_string ltp ^ " : " ^ lexp_string lsort in + -> let tystr = Lexp.to_string ltp ^ " : " ^ Lexp.to_string lsort in match var with - | (l, None) -> lexp_error (sexp_location l) ltp {|"%s" is not a proper type|} tystr + | (l, None) -> lexp_error (Sexp.location l) ltp {|"%s" is not a proper type|} tystr | (l, Some name) - -> lexp_error (sexp_location l) ltp {|Type of "%s" is not a proper type: %s|} name tystr + -> lexp_error (Sexp.location l) ltp {|Type of "%s" is not a proper type: %s|} name tystr let elab_check_proper_type (ctx : elab_context) ltp var = try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp @@ -166,9 +166,9 @@ let elab_check_proper_type (ctx : elab_context) ltp var = ~print_action:(fun _ -> print_lexp_ctx (ectx_to_lctx ctx); print_newline () ) - ~loc:(lexp_location ltp) + ~loc:(Lexp.location ltp) {|Exception while checking type "%s"%s|} - (lexp_string ltp) + (Lexp.to_string ltp) (match var with | (_, None) -> "" | (_, Some name) -> " of var `" ^ name ^ "`"); @@ -188,7 +188,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = print_lexp_ctx (ectx_to_lctx ctx); print_newline () ) - ~loc:(sexp_location loc) + ~loc:(Sexp.location loc) "Error while type-checking"; raise e in if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' @@ -196,10 +196,10 @@ let elab_check_def (ctx : elab_context) var lxp ltype = | e -> info ~print_action:(lexp_print_details lxp) - ~loc:(sexp_location loc) + ~loc:(Sexp.location loc) "Exception while conversion-checking types: %s and %s" - (lexp_string ltype) - (lexp_string ltype'); + (Lexp.to_string ltype) + (Lexp.to_string ltype'); raise e) then elab_check_proper_type ctx ltype var @@ -208,11 +208,11 @@ let elab_check_def (ctx : elab_context) var lxp ltype = ~print_action:(fun _ -> List.iter print_indent_line [ (match var with (_, Some n) -> n | _ -> "<anon>") - ^ " = " ^ lexp_string lxp ^ " !: " ^ lexp_string ltype; + ^ " = " ^ Lexp.to_string lxp ^ " !: " ^ Lexp.to_string ltype; " because"; - lexp_string ltype' ^ " != " ^ lexp_string ltype + Lexp.to_string ltype' ^ " != " ^ Lexp.to_string ltype ]) - ~loc:(sexp_location loc) + ~loc:(Sexp.location loc) "Type check error: ¡¡ctx_define error!!" let ctx_extend (ctx: elab_context) (var : vname) def ltype = @@ -336,13 +336,13 @@ let sdform_define_operator (ctx : elab_context) loc sargs : elab_context = -> let level s = match s with | Symbol (_, "") -> None | Integer (_, n) -> Some (Z.to_int n) - | _ -> sexp_error (sexp_location s) "Expecting an integer or ()"; None in + | _ -> sexp_error (Sexp.location s) "Expecting an integer or ()"; None in let grm = ectx_get_grammar ctx in ectx_set_grammar (Grammar.add name (level l, level r) grm) ctx | [o; _; _] - -> sexp_error (sexp_location o) "Expecting a string"; ctx + -> sexp_error (Sexp.location o) "Expecting a string"; ctx | _ - -> sexp_error (sexp_location loc) "define-operator expects 3 argument"; ctx + -> sexp_error (Sexp.location loc) "define-operator expects 3 argument"; ctx let sform_dummy_ret ctx loc = let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in @@ -362,7 +362,7 @@ let elab_varref ctx (loc, name) if ((List.length xs) > 0) then ". Did you mean: " ^ (String.concat " or " xs) ^" ?" else "" in - sexp_error (sexp_location loc) {|The variable "%s" was not declared%s|} name relateds; + sexp_error (Sexp.location loc) {|The variable "%s" was not declared%s|} name relateds; sform_dummy_ret ctx loc) (* Turn metavar into plain vars after generalization. @@ -573,7 +573,7 @@ let sort_generalized_metavars sl cl ctx mfvs = * `wrap` is the function that adds the relevant quantification, typically * either mkArrow or mkLambda. *) let generalize (nctx : elab_context) e = - let l = lexp_location e in + let l = Lexp.location e in let sl = ectx_to_scope_level nctx in let cl = Myers.length (ectx_to_lctx nctx) in let (_, (mfvs, nes)) = OL.fv e in @@ -613,11 +613,11 @@ let rec sform_immediate ctx loc sargs ot = let (se, _) = sexp_parse_all grm tokens None in elaborate ctx se ot | [_se] - -> (sexp_error (sexp_location loc) ("Non-immediate passed to ##typer-immediate"); - sform_dummy_ret ctx loc) + -> sexp_error (Sexp.location loc) "Non-immediate passed to ##typer-immediate"; + sform_dummy_ret ctx loc | _ - -> (sexp_error (sexp_location loc) ("Too many args to ##typer-immediate"); - sform_dummy_ret ctx loc) + -> sexp_error (Sexp.location loc) "Too many args to ##typer-immediate"; + sform_dummy_ret ctx loc and sform_identifier ctx loc sargs ot = @@ -660,13 +660,13 @@ and sform_identifier ctx loc sargs ot = (* FIXME: The variable is from another scope_level! It means that `subst` is not the right substitution for the metavar! *) - fatal ~loc:(sexp_location loc) ("Bug in the elaboration of a metavar" + fatal ~loc:(Sexp.location loc) ("Bug in the elaboration of a metavar" ^^ " repeated at a different scope level!") | MVal _ -> (* FIXME: We face the same problem as above, but here, the situation is worse, we don't even know the scope level! *) - fatal ~loc:(sexp_location loc) "Bug in the elaboration of a repeated metavar!" + fatal ~loc:(Sexp.location loc) "Bug in the elaboration of a repeated metavar!" else let t = match ot with | None -> newMetatype octx sl loc @@ -678,7 +678,7 @@ and sform_identifier ctx loc sargs ot = let idx = match lexp_lexp' mv with | Metavar (idx, _, _) -> idx - | _ -> fatal ~loc:(sexp_location loc) "newMetavar returned a non-Metavar" in + | _ -> fatal ~loc:(Sexp.location loc) "newMetavar returned a non-Metavar" in rmmap := SMap.add name idx (!rmmap)); (mv, match ot with Some _ -> Checked | None -> Lazy) @@ -687,12 +687,12 @@ and sform_identifier ctx loc sargs ot = -> elab_varref ctx (loc, name) | [_se] - -> (sexp_error (sexp_location loc) ("Non-symbol passed to ##typer-identifier"); - sform_dummy_ret ctx loc) + -> sexp_error (Sexp.location loc) "Non-symbol passed to ##typer-identifier"; + sform_dummy_ret ctx loc | _ - -> (sexp_error (sexp_location loc) ("Too many args to ##typer-identifier"); - sform_dummy_ret ctx loc) + -> sexp_error (Sexp.location loc) "Too many args to ##typer-identifier"; + sform_dummy_ret ctx loc and elab_via head default ctx se ot = match elab_varref ctx head with @@ -715,7 +715,8 @@ and elaborate ctx se ot = (* Rewrite IMM to `typer-immediate IMM`. *) | (Integer _ | Float _ | String _ | Block _) - -> elab_via (se, "typer-immediate") sform_immediate ctx se ot + -> let l = Sexp.location se in + elaborate ctx (Node (l, Symbol (l, "typer-immediate"), [se])) ot | Node (_, se, []) -> elaborate ctx se ot @@ -749,7 +750,7 @@ and elaborate ctx se ot = and infer (p : sexp) (ctx : elab_context): lexp * ltype = match elaborate ctx p None with - | (_, Checked) -> fatal ~loc:(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) @@ -761,7 +762,7 @@ and elab_special_form ctx f args ot = (get_special_form name) ctx loc args ot | _ - -> lexp_error (sexp_location loc) f "Unknown special-form: %s" (lexp_string f); + -> lexp_error (Sexp.location loc) f "Unknown special-form: %s" (Lexp.to_string f); sform_dummy_ret ctx loc and elab_special_decl_form ctx f args = @@ -770,7 +771,7 @@ and elab_special_decl_form ctx f args = | Builtin ((_, name), _) -> (* Special form. *) (get_special_decl_form name) ctx loc args - | _ -> lexp_error (sexp_location loc) f "Unknown special-decl-form: %s" (lexp_string f); ctx + | _ -> lexp_error (Sexp.location loc) f "Unknown special-decl-form: %s" (Lexp.to_string f); ctx (* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = @@ -803,7 +804,7 @@ and sdform_instance (inst : bool) (ctx : elab_context) (_l : sinfo) sargs let (lxp, _) = infer sarg ctx in match lexp_lexp' lxp with | Var (_, idx) -> ectx_set_inst ctx idx inst - | _ -> (lexp_error (lexp_location lxp) lxp + | _ -> (lexp_error (Lexp.location lxp) lxp "Only variables can be instances"; ctx) in List.fold_left make_instance ctx sargs @@ -829,13 +830,13 @@ and infer_type pexp ectx (var: vname) = s (ectx_to_lctx ectx) with | (_::_) - -> (let typestr = lexp_string t ^ " : " ^ lexp_string s in + -> (let typestr = Lexp.to_string t ^ " : " ^ Lexp.to_string s in match var with | (l, None) - -> lexp_error (sexp_location l) t {|"%s" is not a proper type|} typestr + -> lexp_error (Sexp.location l) t {|"%s" is not a proper type|} typestr | (l, Some name) -> lexp_error - (sexp_location l) t {|Type of "%s" is not a proper type: %s|} name typestr) + (Sexp.location l) t {|Type of "%s" is not a proper type: %s|} name typestr) | [] -> ()); t @@ -854,8 +855,8 @@ and unify_with_arrow ctx tloc lxp kind var aty match Unif.unify arrow lxp (ectx_to_lctx ctx) with | ((_ck, _ctx, t1, t2)::_) -> lexp_error - (sexp_location tloc) lxp {|Types:\n %s\n and:\n %s\n do not match!|} - (lexp_string t1) (lexp_string t2); + (Sexp.location tloc) lxp {|Types:\n %s\n and:\n %s\n do not match!|} + (Lexp.to_string t1) (Lexp.to_string t2); (mkDummy_type ctx l, mkDummy_type nctx l) | [] -> arg, body @@ -866,18 +867,18 @@ and unify_or_error lctx lxp ?lxp_name expect actual = match Unif.unify expect actual lctx with | ((ck, _ctx, t1, t2)::_) -> lexp_error - (lexp_location lxp) lxp + (Lexp.location lxp) lxp ({|Type mismatch%s! Context expected:\n%s|} ^^ {|\nbut %s has type:\n %s\n|} ^^ {|can't unify:\n %s\nwith:\n %s|}) (match ck with | Unif.CKimpossible -> "" | Unif.CKresidual -> " (residue)") - (lexp_string expect) + (Lexp.to_string expect) (Option.value ~default:"expression" lxp_name) - (lexp_string actual) - (lexp_string t1) - (lexp_string t2); + (Lexp.to_string actual) + (Lexp.to_string t1) + (Lexp.to_string t2); assert (not (OL.conv_p lctx expect actual)) | [] -> () @@ -898,7 +899,7 @@ and check_inferred ctx e inferred_t t = and check_case rtype (loc, target, ppatterns) ctx = (* Helpers *) - let pat_string p = sexp_string (pexp_u_pat p) in + let pat_string p = Sexp.to_string (pexp_u_pat p) in let uniqueness_warn pat = warning @@ -924,8 +925,8 @@ and check_case rtype (loc, target, ppatterns) ctx = match Unif.unify actual expected (ectx_to_lctx ctx) with | (_::_) -> lexp_error - (sexp_location loc) lctor {|Expected pattern of type "%s", but got "%s"|} - (lexp_string expected) (lexp_string actual) + (Sexp.location loc) lctor {|Expected pattern of type "%s", but got "%s"|} + (Lexp.to_string expected) (Lexp.to_string actual) | [] -> () in match !it_cs_as with | Some (it, cs, args) @@ -959,8 +960,8 @@ and check_case rtype (loc, target, ppatterns) ctx = constructors | _ -> lexp_error - (sexp_location target) tlxp - {|Can't "case" on objects of type "%s"|} (lexp_string tltp); + (Sexp.location target) tlxp + {|Can't "case" on objects of type "%s"|} (Lexp.to_string tltp); SMap.empty in it_cs_as := Some (it, constructors, targs); (constructors, targs) in @@ -996,7 +997,7 @@ and check_case rtype (loc, target, ppatterns) ctx = lbranches, Some (v, lexp) in let add_branch pctor pargs = - let loc = sexp_location pctor in + let loc = Sexp.location pctor in let lctor, _ct = infer pctor ctx in let rec inst_args ctx e = let lxp = OL.lexp_whnf e (ectx_to_lctx ctx) in @@ -1017,7 +1018,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | Not_found -> lexp_error loc lctor {|"%s" does not a have a "%s" constructor|} - (lexp_string it') cons_name; + (Lexp.to_string it') cons_name; [] in let subst = List.fold_left (fun s (_, t) -> S.cons t s) @@ -1091,7 +1092,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | Ppatsym ((_, None) as var) -> add_default var | Ppatsym ((l, Some name) as var) -> if Eval.constructor_p name ctx then - add_branch (Symbol (sexp_location l, name)) [] + add_branch (Symbol (Sexp.location l, name)) [] else add_default var (* A named default branch. *) | Ppatcons (_, pctor, pargs) -> add_branch pctor pargs in @@ -1117,15 +1118,15 @@ and elab_macro_call if !macro_tracing_enabled then - (trace_macro ~location:(sexp_location location) {|expanding: %s|} (lexp_string func); + (trace_macro ~location:(Sexp.location location) {|expanding: %s|} (Lexp.to_string func); List.iteri (fun i arg -> - arg |> sexp_string |> trace_macro ~location:(sexp_location location) {|input %d: %s|} i) + arg |> Sexp.to_string |> trace_macro ~location:(Sexp.location location) {|input %d: %s|} i) args); let sxp = lexp_expand_macro location func args ctx (Some t) in if !macro_tracing_enabled - then trace_macro ~location:(sexp_location location) {|output: %s|} (sexp_string sxp); + then trace_macro ~location:(Sexp.location location) {|output: %s|} (Sexp.to_string sxp); elaborate ctx sxp ot @@ -1142,7 +1143,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = let larg = check sarg arg_type ctx in handle_fun_args ((ak, larg) :: largs) sargs (SMap.remove aname pending) - (L.mkSusp ret_type (S.substitute larg)) + (Lexp.mkSusp ret_type (S.substitute larg)) | Node (_, Symbol (_, "_:=_"), [Symbol (_, aname); sarg]) :: sargs, Arrow (_, ak, _, arg_type, ret_type) @@ -1150,7 +1151,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = (* Explicit-implicit argument. *) -> let larg = check sarg arg_type ctx in handle_fun_args ((ak, larg) :: largs) sargs pending - (L.mkSusp ret_type (S.substitute larg)) + (Lexp.mkSusp ret_type (S.substitute larg)) | Node (_, Symbol (_, "_:=_"), [Symbol (l, aname); sarg]) :: sargs, Arrow _ @@ -1161,7 +1162,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = | Node (_, Symbol (_, "_:=_"), Symbol (l, aname) :: _) :: sargs, _ -> sexp_error l {|Explicit arg "%s" to non-function (type = %s)|} - aname (lexp_string ltp); + aname (Lexp.to_string ltp); handle_fun_args largs sargs pending ltp (* Aerasable *) @@ -1172,12 +1173,12 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = -> let arg_loc = try (List.hd sargs) with _ -> loc in let larg = newInstanceMetavar ctx (arg_loc, v) arg_type in handle_fun_args ((ak, larg) :: largs) sargs pending - (L.mkSusp ret_type (S.substitute larg)) + (Lexp.mkSusp ret_type (S.substitute larg)) | [], _ -> (if not (SMap.is_empty pending) then let pending = SMap.bindings pending in let loc = match pending with - | (_, sarg)::_ -> sexp_location sarg + | (_, sarg)::_ -> Sexp.location sarg | _ -> assert false in lexp_error loc func {|Explicit actual args "%s" have no matching formal args|} @@ -1192,7 +1193,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = ltp' Anormal (sarg, None) None in let larg = check sarg arg_type ctx in handle_fun_args ((Anormal, larg) :: largs) sargs pending - (L.mkSusp ret_type (S.substitute larg)) in + (Lexp.mkSusp ret_type (S.substitute larg)) in let (largs, ret_type) = handle_fun_args [] sargs SMap.empty ltp in (mkCall (loc, func, List.rev largs), Inferred ret_type) @@ -1269,8 +1270,8 @@ and lexp_eval ectx e = if not (EV.closed_p rctx (OL.fv e)) then lexp_error - (lexp_location e) e {|Expression "%s" is not closed: %s|} - (lexp_string e) (track_fv rctx (ectx_to_lctx ectx) e); + (Lexp.location e) e {|Expression "%s" is not closed: %s|} + (Lexp.to_string e) (track_fv rctx (ectx_to_lctx ectx) e); try EV.eval ee rctx with exc -> @@ -1292,16 +1293,16 @@ and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) let args = [macro; BI.o2v_list sargs] in (* FIXME: Make a proper `Var`. *) - let value = EV.eval_call (sexp_location loc) (EL.Var ((dsinfo, Some "expand_macro"), 0)) + let value = EV.eval_call (Sexp.location loc) (EL.Var ((dsinfo, Some "expand_macro"), 0)) ([], []) macro_expand args in match value with | Vcommand cmd -> (match cmd () with | Vsexp sxp -> sxp - | v -> value_fatal (sexp_location loc) v "Macro `%s` should return an IO sexp" - (lexp_string macro_funct)) - | v -> value_fatal (sexp_location loc) v "Macro `%s` should return an IO" - (lexp_string macro_funct) + | v -> value_fatal (Sexp.location loc) v "Macro `%s` should return an IO sexp" + (Lexp.to_string macro_funct)) + | v -> value_fatal (Sexp.location loc) v "Macro `%s` should return an IO" + (Lexp.to_string macro_funct) (* Print each generated decls *) @@ -1452,7 +1453,7 @@ and lexp_decls_1 loc ltp {|New type annotation "%s" incompatible with previous "%s"|} - (lexp_string ltp) (lexp_string pt) + (Lexp.to_string ltp) (Lexp.to_string pt) | [] -> () in recur [] nctx pending_decls pending_defs else if List.exists (fun ((_, vname'), _) -> vname = vname') @@ -1466,7 +1467,7 @@ and lexp_decls_1 | _ -> error ~loc {|Invalid type declaration syntax : "%s"|} - (sexp_string thesexp); + (Sexp.to_string thesexp); recur [] nctx pending_decls pending_defs) | Some (Node (_, (Symbol (loc, "_=_") as head), args) as thesexp) @@ -1505,13 +1506,13 @@ and lexp_decls_1 head, [Symbol s; Node (location, - Symbol (sexp_location d, "lambda_->_"), + Symbol (Sexp.location d, "lambda_->_"), [sexp_u_list args location; body])])] nctx pending_decls pending_defs | _ -> error - ~loc {|Invalid definition syntax : "%s"|} (sexp_string thesexp); + ~loc {|Invalid definition syntax : "%s"|} (Sexp.to_string thesexp); recur [] nctx pending_decls pending_defs) | Some sexp @@ -1529,7 +1530,7 @@ and lexp_decls_1 let sdecl' = lexp_expand_macro sxp lxp sargs nctx None in recur [sdecl'] nctx pending_decls pending_defs else ( - error ~loc:(sexp_location sxp) "Invalid declaration syntax"; + error ~loc:(Sexp.location sxp) "Invalid declaration syntax"; recur [] nctx pending_decls pending_defs ) @@ -1573,9 +1574,9 @@ and sform_declexpr ctx loc sargs _ot = | [e] when is_var e -> (match DB.env_lookup_expr ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)) with | Some lxp -> (lxp, Lazy) - | None -> error ~loc:(sexp_location loc) "no expr available"; + | None -> error ~loc:(Sexp.location loc) "no expr available"; sform_dummy_ret ctx loc) - | _ -> error ~loc:(sexp_location loc) "declexpr expects one argument"; + | _ -> error ~loc:(Sexp.location loc) "declexpr expects one argument"; sform_dummy_ret ctx loc @@ -1583,7 +1584,7 @@ let sform_decltype ctx loc sargs _ot = match List.map (lexp_parse_sexp ctx) sargs with | [e] when is_var e -> (DB.env_lookup_type ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)), Lazy) - | _ -> error ~loc:(sexp_location loc) "decltype expects one argument"; + | _ -> error ~loc:(Sexp.location loc) "decltype expects one argument"; sform_dummy_ret ctx loc @@ -1599,19 +1600,19 @@ let sform_built_in ctx loc sargs ot = * function. It's not indispensible, tho it might still be useful for * performance of type-inference (at least until we have proper * memoization of push_susp and/or whnf). *) - -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in - let bi = mkBuiltin ((sexp_location loc, name), ltp') in + -> let ltp' = Lexp.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in + let bi = mkBuiltin ((Sexp.location loc, name), ltp') in if not (SMap.mem name (!EV.builtin_functions)) then - sexp_error (sexp_location loc) {|Unknown built-in "%s"|} name; + sexp_error (Sexp.location loc) {|Unknown built-in "%s"|} name; BI.add_builtin_cst name bi; (bi, Checked) - | None -> error ~loc:(sexp_location loc) "Built-in's type not provided by context!"; + | None -> error ~loc:(Sexp.location loc) "Built-in's type not provided by context!"; sform_dummy_ret ctx loc) - | true, _ -> error ~loc:(sexp_location loc) "Wrong Usage of `Built-in`"; + | true, _ -> error ~loc:(Sexp.location loc) "Wrong Usage of `Built-in`"; sform_dummy_ret ctx loc - | false, _ -> error ~loc:(sexp_location loc) "Use of `Built-in` in user code"; + | false, _ -> error ~loc:(Sexp.location loc) "Use of `Built-in` in user code"; sform_dummy_ret ctx loc let sform_datacons ctx loc sargs _ot = @@ -1620,9 +1621,9 @@ let sform_datacons ctx loc sargs _ot = -> let idt, _ = infer t ctx in (mkCons (idt, sym), Lazy) - | [_;_] -> sexp_error (sexp_location loc) "Second arg of ##constr should be a symbol"; + | [_;_] -> sexp_error (Sexp.location loc) "Second arg of ##constr should be a symbol"; sform_dummy_ret ctx loc - | _ -> sexp_error (sexp_location loc) "##constr requires two arguments"; + | _ -> sexp_error (Sexp.location loc) "##constr requires two arguments"; sform_dummy_ret ctx loc let elab_colon_to_ak k = match k with @@ -1641,21 +1642,21 @@ let elab_typecons_arg arg : (arg_kind * vname * sexp option) = -> (elab_colon_to_ak k, (arg, Some name), Some e) | Symbol (_l, name) -> (Anormal, (arg, Some name), None) - | _ -> sexp_error ~print_action:(fun _ -> sexp_print arg; print_newline ()) - (sexp_location arg) + | _ -> sexp_error ~print_action:(fun _ -> Sexp.print arg; print_newline ()) + (Sexp.location arg) "Unrecognized formal arg"; (Anormal, (arg, None), None) let sform_typecons ctx loc sargs _ot = match sargs with - | [] -> sexp_error (sexp_location loc) "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) + | [] -> sexp_error (Sexp.location loc) "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) | formals :: constrs -> let (label, formals) = match formals with | Node (_, label, formals) -> (label, formals) | _ -> (formals, []) in let label = match label with | Symbol label -> label - | _ -> let loc = sexp_location label in + | _ -> let loc = Sexp.location label in sexp_error loc "Unrecognized inductive type name"; (loc, "<error>") in @@ -1684,7 +1685,7 @@ let sform_typecons ctx loc sargs _ot = (* This is a constructor with no args *) | Symbol s -> (s, [])::pcases - | _ -> sexp_error (sexp_location case) + | _ -> sexp_error (Sexp.location case) "Unrecognized constructor declaration"; pcases) constrs [] in @@ -1697,7 +1698,7 @@ let sform_hastype ctx loc sargs _ot = | [se; st] -> let lt = infer_type st ctx (loc, None) in let le = check se lt ctx in (le, Inferred lt) - | _ -> sexp_error (sexp_location loc) "##_:_ takes two arguments"; + | _ -> sexp_error (Sexp.location loc) "##_:_ takes two arguments"; sform_dummy_ret ctx loc let sform_arrow kind ctx loc sargs _ot = @@ -1710,7 +1711,7 @@ let sform_arrow kind ctx loc sargs _ot = let nctx = ectx_extend ctx v Variable lt1 in let lt2 = infer_type st2 nctx (st2, None) in (mkArrow (loc, kind, v, lt1, lt2), Lazy) - | _ -> sexp_error (sexp_location loc) "##_->_ takes two arguments"; + | _ -> sexp_error (Sexp.location loc) "##_->_ takes two arguments"; sform_dummy_ret ctx loc let rec sform_lambda kind ctx loc sargs ot = @@ -1719,7 +1720,7 @@ let rec sform_lambda kind ctx loc sargs ot = -> let (arg, ost1) = match sarg with | Node (_, Symbol (_, "_:_"), [Symbol arg; st]) -> (elab_p_id arg, Some st) | Symbol arg -> (elab_p_id arg, None) - | _ -> sexp_error (sexp_location sarg) + | _ -> sexp_error (Sexp.location sarg) "Unrecognized lambda argument"; ((dsinfo, None), None) in @@ -1782,7 +1783,7 @@ let rec sform_lambda kind ctx loc sargs ot = | _ -> sexp_error - (sexp_location loc) "##lambda_%s_ takes two arguments" + (Sexp.location loc) "##lambda_%s_ takes two arguments" (match kind with | Anormal -> "->" | Aimplicit -> "=>" @@ -1794,7 +1795,7 @@ let rec sform_case ctx sinfo sargs ot = match sargs with -> let parse_case branch = match branch with | Node (_, Symbol (_, "_=>_"), [pat; code]) -> (pexp_p_pat pat, code) - | _ -> let l = (sexp_location branch) in + | _ -> let l = (Sexp.location branch) in sexp_error l "Unrecognized simple case branch"; (Ppatsym (se, None), Symbol (l, "?")) in let pcases = List.map parse_case scases in @@ -1806,10 +1807,10 @@ let rec sform_case ctx sinfo sargs ot = match sargs with (* In case there are no branches, pretend there was a | anyway. *) | [_e] - -> let loc = sexp_location sinfo in + -> let loc = Sexp.location sinfo in sform_case ctx sinfo [Node (loc, Symbol (loc, "_|_"), sargs)] ot | _ - -> sexp_error (sexp_location sinfo) "Unrecognized case expression"; + -> sexp_error (Sexp.location sinfo) "Unrecognized case expression"; sform_dummy_ret ctx sinfo let sform_letin ctx loc sargs ot = match sargs with @@ -1825,7 +1826,7 @@ let sform_letin ctx loc sargs ot = match sargs with | Inferred t -> Inferred (mkSusp t s) | _ -> ot in (lexp_let_decls declss bdy nctx, ot) - | _ -> sexp_error (sexp_location loc) "Unrecognized let_in_ expression"; + | _ -> sexp_error (Sexp.location loc) "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc let sform_proj ctx loc sargs _ = @@ -1835,9 +1836,9 @@ let sform_proj ctx loc sargs _ = let e = mkProj (loc,ret,(loca,str)) in (e, Lazy) | [_;_] - -> sexp_error (sexp_location loc) "Second argument is not a Symbol!"; + -> sexp_error (Sexp.location loc) "Second argument is not a Symbol!"; sform_dummy_ret ctx loc - | _ -> sexp_error (sexp_location loc) "Wrong arg number!"; + | _ -> sexp_error (Sexp.location loc) "Wrong arg number!"; sform_dummy_ret ctx loc let rec infer_level ctx se : lexp = @@ -1848,8 +1849,8 @@ let rec infer_level ctx se : lexp = -> mkSortLevel (SLsucc (infer_level ctx se)) | Node (_, Symbol (_, "_∪_"), [se1; se2]) -> OL.mkSLlub (ectx_to_lctx ctx) (infer_level ctx se1) (infer_level ctx se2) - | _ -> let l = (sexp_location se) in - (sexp_error l "Unrecognized TypeLevel: %s" (sexp_string se); + | _ -> let l = (Sexp.location se) in + (sexp_error l "Unrecognized TypeLevel: %s" (Sexp.to_string se); newMetalevel (ectx_to_lctx ctx) (ectx_to_scope_level ctx) se) (* Actually `Type_` could also be defined as a plain constant @@ -1863,7 +1864,7 @@ let sform_type ctx loc sargs _ot = | [se] -> let l = infer_level ctx se in (mkSort (loc, Stype l), Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l))))) - | _ -> (sexp_error (sexp_location loc) "##Type_ expects one argument"; + | _ -> (sexp_error (Sexp.location loc) "##Type_ expects one argument"; sform_dummy_ret ctx loc) let sform_debruijn ctx loc sargs _ot = @@ -1874,7 +1875,7 @@ let sform_debruijn ctx loc sargs _ot = sform_dummy_ret ctx loc) else let lxp = mkVar ((loc, None), i) in (lxp, Lazy) - | _ -> (sexp_error (sexp_location loc) "##DeBruijn expects one integer argument"; + | _ -> (sexp_error (Sexp.location loc) "##DeBruijn expects one integer argument"; sform_dummy_ret ctx loc) (* Only print var info *) @@ -1889,9 +1890,9 @@ let lexp_print_var_info ctx = print_string " = "; (match exp with | None -> print_string "<var>" - | Some exp -> lexp_print exp); + | Some exp -> Lexp.print exp); print_string ": "; - lexp_print tp; + Lexp.print tp; print_string "\n") done @@ -1910,7 +1911,7 @@ let sform_load usr_elctx loc sargs _ot = let pres = try prelex source with | Sys_error _ - -> error ~loc:(sexp_location loc) {|Could not load "%s": file not found.|} file_name; [] + -> error ~loc:(Sexp.location loc) {|Could not load "%s": file not found.|} file_name; [] in let sxps = lex default_stt pres in let _, elctx = lexp_p_decls [] sxps elctx @@ -1922,7 +1923,7 @@ let sform_load usr_elctx loc sargs _ot = read_file file_name usr_elctx else read_file file_name !sform_default_ectx - | _ -> (error ~loc:(sexp_location loc) "argument to load should be one file name (String)"; + | _ -> (error ~loc:(Sexp.location loc) "argument to load should be one file name (String)"; !sform_default_ectx) in (* get lexp_context *) ===================================== src/elexp.ml ===================================== @@ -30,17 +30,9 @@ * * --------------------------------------------------------------------------- *) +open Sexp -open Sexp (* Sexp type *) - -module U = Util -module L = Lexp - -type vname = Sexp.vname -type vref = Sexp.vref -type label = symbol - -module SMap = U.SMap +module SMap = Util.SMap type elexp = (* A constant, either string, integer, or float. *) @@ -52,10 +44,10 @@ type elexp = (* A variable reference, using deBruijn indexing. *) | Var of vref - | Proj of U.location * elexp * int + | Proj of Source.Location.t * elexp * int (* Recursive `let` binding. *) - | Let of U.location * (vname * elexp) list * elexp + | Let of Source.Location.t * eldecls * elexp (* An anonymous function. *) | Lambda of vname * elexp @@ -73,86 +65,89 @@ type elexp = * Case (l, e, branches, default) * tests the value of `e`, and either selects the corresponding branch * in `branches` or branches to the `default`. *) - | Case of U.location * elexp - * (U.location * vname list * elexp) SMap.t + | Case of Source.Location.t + * elexp + * (Source.Location.t * vname list * elexp) SMap.t * (vname * elexp) option (* A Type expression. There's no useful operation we can apply to it, * but they can appear in the code. *) - | Type of L.lexp - -let rec elexp_location e = - match e with - | Imm s -> sexp_location s - | Var ((l,_), _) -> sexp_location l - | Proj (l,_,_) -> l - | Builtin ((l, _)) -> l - | Let (l,_,_) -> l - | Lambda ((l,_),_) -> sexp_location l - | Call (f,_) -> elexp_location f - | Cons (_, (l, _)) -> l - | Case (l,_,_,_) -> l - | Type e -> L.lexp_location e - - -let elexp_name e = + | Type of Lexp.lexp + +and eldecl = vname * elexp +and eldecls = eldecl list + +let rec location : elexp -> Source.Location.t = function + | Imm s -> Sexp.location s + | Var ((l, _), _) -> Sexp.location l + | Proj (l, _, _) -> l + | Builtin ((l, _)) -> l + | Let (l, _, _) -> l + | Lambda ((l, _), _) -> Sexp.location l + | Call (f, _) -> location f + | Cons (_, (l, _)) -> l + | Case (l, _, _, _) -> l + | Type (e) -> Lexp.location e + +let rec pp_print (f : Format.formatter) (e : elexp) : unit = + let open Format in match e with - | Imm _ -> "Imm" - | Var _ -> "Var" - | Proj _ -> "Proj" - | Let _ -> "Let" - | Call _ -> "Call" - | Cons _ -> "Cons" - | Case _ -> "Case" - | Type _ -> "Type" - | Lambda _ -> "Lambda" - | Builtin _ -> "Builtin" - -let rec elexp_print lxp = print_string (elexp_string lxp) -and elexp_string lxp = - let maybe_str lxp = - match lxp with - | Some (v, lxp) - -> " | " ^ (match v with (_, None) -> "_" | (_, Some name) -> name) - ^ " => " ^ elexp_string lxp - | None -> "" in - - let str_decls d = - List.fold_left (fun str ((_, s), lxp) -> - str ^ " " ^ L.maybename s ^ " = " ^ (elexp_string lxp)) "" d in - - let str_pat lst = - List.fold_left (fun str v -> - str ^ " " ^ (match v with - | (_, None) -> "_" - | (_, Some s) -> s)) "" lst in - - let str_cases c = - SMap.fold (fun key (_, lst, lxp) str -> - str ^ " | " ^ key ^ " " ^ (str_pat lst) ^ " => " ^ (elexp_string lxp)) - c "" in - - let str_args lst = - List.fold_left (fun str lxp -> - str ^ " " ^ (elexp_string lxp)) "" lst in - - match lxp with - | Imm(s) -> sexp_string s - | Builtin((_, s)) -> s - | Var((_, s), i) -> L.maybename s ^ "[" ^ string_of_int i ^ "]" - | Proj (_,lxp,i) - -> "( __.__ " ^ elexp_string lxp ^ " " ^ (string_of_int i) ^ " )" - | Cons (_, (_, s)) -> "datacons(" ^ s ^")" - - | Lambda((_, s), b) -> "lambda " ^ L.maybename s ^ " -> " ^ (elexp_string b) - - | Let(_, d, b) -> - "let" ^ (str_decls d) ^ " in " ^ (elexp_string b) - - | Call(fct, args) -> - "(" ^ (elexp_string fct) ^ (str_args args) ^ ")" - - | Case(_, t, cases, default) -> - "case " ^ (elexp_string t) ^ (str_cases cases) ^ (maybe_str default) - - | Type e -> "Type(" ^ L.lexp_string e ^ ") " + | Imm (value) + -> Sexp.pp_print f value + + | Var (name, index) + -> Lexp.pp_print_var f name index + + | Proj (_, e, field_name) + -> Lexp.pp_print_proj f pp_print e pp_print_int field_name + + | Builtin (name) + -> Lexp.pp_print_builtin f name + + | Let (_, decls, body) + -> Lexp.pp_print_let f pp_print_decl_block decls pp_print body + + | Lambda (param_name, body) + -> Lexp.pp_print_lambda + f + (fun f param_name + -> fprintf f "(%a)" (Sexp.pp_print_vname ~default:"_") param_name) + param_name + Pexp.Anormal + pp_print + body + + | Call (callee, args) + -> Lexp.pp_print_call f pp_print callee pp_print args + + | Cons (_, name) + -> fprintf f "@{<magenta>datacons@}@ %a" Sym.pp_print name + + | Case (_, e, branches, default) + -> Lexp.pp_print_case + f pp_print e (Sexp.pp_print_vname ~default:"_") branches default + + | Type (e) + -> fprintf f "Type(%a)" Lexp.pp_print e + +and pp_print_decl_block (f : Format.formatter) (decls : eldecls) : unit = + let open Format in + let pp_print_decl (f : Format.formatter) (name, body : eldecl) : unit = + fprintf f "@[<hov 2>%s =@ %a;@]" (string_of_vname name) pp_print body + in + fprintf + f + "@[<v 0>%a@]" + (pp_print_list ~pp_sep:pp_print_space pp_print_decl) + decls + +let pp_print_decls (f : Format.formatter) (eldecls : eldecls list) : unit = + let open Format in + fprintf + f + "@[<v 0>%a@]" + (pp_print_list ~pp_sep:pp_print_cut pp_print_decl_block) + eldecls + +let to_string : elexp -> string = + Format.asprintf "%a" pp_print ===================================== src/env.ml ===================================== @@ -30,20 +30,14 @@ * * --------------------------------------------------------------------------- *) -open Printf - +open Elexp open Fmt (* make_title, table util *) - +open Printf open Sexp -open Elexp module M = Myers -module L = Lexp -module BI = Z (* Was Big_int *) module DB = Debruijn -let dloc = Util.dummy_location - let fatal ?print_action ?loc fmt = Log.log_fatal ~section:"ENV" ?print_action ?loc fmt let warning ?print_action ?loc fmt = @@ -53,7 +47,7 @@ let str_idx idx = "[" ^ (string_of_int idx) ^ "]" type value_type = | Vint of int - | Vinteger of BI.t + | Vinteger of Z.t | Vstring of string | Vcons of symbol * value_type list | Vbuiltin of string @@ -62,7 +56,7 @@ type value_type = | Vsexp of sexp (* Values passed to macros. *) (* Unable to eval during macro expansion, only throw if the value is used *) | Vundefined - | Vtype of L.lexp (* The lexp value can't be trusted. *) + | Vtype of Lexp.lexp (* The lexp value can't be trusted. *) | Vin of in_channel | Vout of out_channel | Vcommand of (unit -> value_type) @@ -115,12 +109,11 @@ let rec value_eq_list a b = | v1::vv1, v2::vv2 -> value_equal v1 v2 && value_eq_list vv1 vv2 | _ -> false -let value_location (vtp: value_type) = - match vtp with - | Vcons ((loc, _), _) -> loc - | Closure (_, lxp, _) -> elexp_location lxp - (* location info was lost or never existed *) - | _ -> dloc +let value_location : value_type -> Source.Location.t = function + | Vcons ((loc, _), _) -> loc + | Closure (_, lxp, _) -> Elexp.location lxp + (* location info was lost or never existed *) + | _ -> Source.Location.dummy let rec value_name v = match v with @@ -150,11 +143,12 @@ let rec value_string v = | Vstring s -> "\"" ^ s ^ "\"" | Vbuiltin s -> s | Vint i -> string_of_int i - | Vinteger i -> BI.to_string i + | Vinteger i -> Z.to_string i | Vfloat f -> string_of_float f - | Vsexp s -> sexp_string s - | Vtype e -> L.lexp_string e - | Closure ((_, s), elexp, _) -> "(lambda " ^ L.maybename s ^ " -> " ^ (elexp_string elexp) ^ ")" + | Vsexp s -> Sexp.to_string s + | Vtype e -> Lexp.to_string e + | Closure ((_, s), elexp, _) + -> "(lambda " ^ Lexp.maybename s ^ " -> " ^ Elexp.to_string elexp ^ ")" | Vcons ((_, s), lst) -> let args = List.fold_left (fun str v -> str ^ " " ^ value_string v) @@ -202,7 +196,7 @@ let print_rte_ctx_n (ctx: runtime_env) start = (* Only print user defined variables *) let print_rte_ctx ctx = - print_rte_ctx_n ctx (!L.builtin_size) + print_rte_ctx_n ctx (!Lexp.builtin_size) (* Dump the whole context *) let dump_rte_ctx ctx = @@ -246,7 +240,7 @@ let set_rte_variable idx name (v: value_type) (ctx : runtime_env) = let nfirst_rte_var n ctx = let rec loop i acc = if i < n then - loop (i + 1) ((get_rte_variable L.vdummy i ctx)::acc) + loop (i + 1) ((get_rte_variable Lexp.vdummy i ctx)::acc) else List.rev acc in loop 0 [] ===================================== src/eval.ml ===================================== @@ -44,10 +44,6 @@ open Env open Printf (* IO Monad *) module OL = Opslexp -module Lexer = Lexer (* lex *) -module Prelexer = Prelexer (* prelex_string *) - - type eval_debug_info = elexp list * elexp list let dloc = dummy_location @@ -109,8 +105,8 @@ let warning loc ?print_action fmt = let root_string () = let a, _ = !global_eval_trace in match List.rev a with - | [] -> "" - | e::_ -> elexp_string e + | [] -> "" + | e :: _ -> Elexp.to_string e let trace_value (value : value_type) : string = sprintf @@ -120,10 +116,10 @@ let trace_value (value : value_type) : string = (root_string ()) let trace_elexp (elexp : elexp) : string = - sprintf - "\t> %s : %s\n\t> Root: %s\n" - (elexp_name elexp) - (elexp_string elexp) + Format.asprintf + "\t>%a\n\t> Root: %s\n" + Elexp.pp_print + elexp (root_string ()) (* FIXME: We're not using predef here. This will break if we change @@ -251,10 +247,10 @@ let add_binary_biop name f = | _ -> error loc {|"%s" expects 2 Integer arguments|} name in add_builtin_function name f 2 -let _ = add_binary_biop "+" BI.add; - add_binary_biop "-" BI.sub; - add_binary_biop "*" BI.mul; - add_binary_biop "/" BI.div +let _ = add_binary_biop "+" Z.add; + add_binary_biop "-" Z.sub; + add_binary_biop "*" Z.mul; + add_binary_biop "/" Z.div let add_binary_bool_biop name f = let name = "Integer." ^ name in @@ -264,17 +260,17 @@ let add_binary_bool_biop name f = | _ -> error loc {|"%s" expects 2 Integer arguments|} name in add_builtin_function name f 2 -let _ = add_binary_bool_biop "<" BI.lt; - add_binary_bool_biop ">" BI.gt; - add_binary_bool_biop "=" BI.equal; - add_binary_bool_biop ">=" BI.geq; - add_binary_bool_biop "<=" BI.leq; +let _ = add_binary_bool_biop "<" Z.lt; + add_binary_bool_biop ">" Z.gt; + add_binary_bool_biop "=" Z.equal; + add_binary_bool_biop ">=" Z.geq; + add_binary_bool_biop "<=" Z.leq; let name = "Int->Integer" in add_builtin_function name (fun loc (_depth : eval_debug_info) (args_val: value_type list) -> match args_val with - | [Vint v] -> Vinteger (BI.of_int v) + | [Vint v] -> Vinteger (Z.of_int v) | _ -> error loc {|"%s" expects 1 Int argument|} name) 1; let name = "Integer->Int" in @@ -283,7 +279,7 @@ let _ = add_binary_bool_biop "<" BI.lt; (fun loc (_depth : eval_debug_info) (args_val: value_type list) -> match args_val with | [Vinteger v] - -> (try Vint (BI.to_int v) with + -> (try Vint (Z.to_int v) with | Z.Overflow -> error loc {|Overflow in "%s"|} name) | _ -> error loc {|"%s" expects 1 Integer argument|} name) 1 @@ -385,10 +381,11 @@ let sexp_eq loc _depth args_val = match args_val with | [Vsexp (s1); Vsexp (s2)] -> o2v_bool (sexp_equal s1 s2) | _ -> error loc "Sexp.= expects 2 sexps" -let sexp_debug_print loc _depth args_val = match args_val with - | [Vsexp (s1)] -> (let tstr = sexp_name s1 - in (print_string ("\n\t"^tstr^" : ["^(sexp_string s1)^"]\n\n") - ; Vcommand (fun () -> Vsexp (s1)))) +let sexp_debug_print loc _depth = function + | [Vsexp (s1)] + -> let tstr = sexp_name s1 in + Format.printf "\n\t%s : [%a]\n\n" tstr Sexp.pp_print s1; + Vcommand (fun () -> Vsexp (s1)) | _ -> error loc "Sexp.debug_print expects 1 sexps" let file_open loc _depth args_val = match args_val with @@ -459,7 +456,7 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) (* Function call *) | Call (f, args) - -> eval_call (elexp_location f) f trace + -> eval_call (Elexp.location f) f trace (eval f ctx trace) (List.map (fun e -> eval e ctx trace) args) (* Proj *) @@ -467,7 +464,7 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) -> (match eval' e ctx with | Vcons (_, vtl) -> List.nth vtl i | _ -> error loc "Proj on a non-datatype constructor: %s \n" - (elexp_string e)) + (Elexp.to_string e)) (* Case *) | Case (loc, target, pat, dflt) -> (eval_case ctx trace loc target pat dflt) @@ -490,14 +487,13 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) and eval_var ctx lxp v = - let (loc, name as vname, idx) = v in - try get_rte_variable vname idx ctx - with + let ((sinfo, name as vname), idx) = v in + try get_rte_variable vname idx ctx with | _e -> Log.log_fatal - ~loc:(sexp_location loc) - "Variable: %s%d was not found\n%s" - (L.maybename name) idx (trace_elexp lxp) + ~loc:(Sexp.location sinfo) + "Variable: %s[%d] was not found\n%s" + (Lexp.maybename name) idx (trace_elexp lxp) (* unef: unevaluated function (to make the trace readable) *) and eval_call loc unef i f args = @@ -558,7 +554,7 @@ and eval_call loc unef i f args = (* We may call a Vlexp e.g. for "x = Map Int String". * FIXME: The arg will sometimes be a Vlexp but not always, so this is * really just broken! *) - -> Vtype (L.mkCall (dsinfo, e, [(Anormal, mkVar (vdummy, -1))])) + -> Vtype (Lexp.mkCall (dsinfo, e, [(Pexp.Anormal, mkVar (vdummy, -1))])) | _ -> fatal loc "Trying to call a non-function!\n%s" (trace_value f) and eval_case ctx i loc target pat dflt = @@ -571,7 +567,7 @@ and eval_case ctx i loc target pat dflt = | _ -> error loc {|Target "%s" is not a Constructor\n%s|} - (elexp_string target) (trace_value v) + (Elexp.to_string target) (trace_value v) in (* Get working pattern *) @@ -673,7 +669,7 @@ and print_typer_trace' trace = let _ = List.iteri (fun i expr -> print_string " "; Fmt.print_ct_tree i; print_string "+- "; - print_string ((elexp_string expr) ^ "\n")) trace in + print_string ((Elexp.to_string expr) ^ "\n")) trace in print_string (Fmt.make_sep '=') @@ -693,7 +689,7 @@ and print_trace title trace default = let trace = List.rev trace in (* Now eval trace and elab trace are the same *) - let print_trace = (fun type_name type_string type_loc i expr -> + let print_trace = (fun type_string type_loc i expr -> (* Print location info *) print_string (" [" ^ (Source.Location.to_string (type_loc expr)) ^ "] "); @@ -701,10 +697,10 @@ and print_trace title trace default = Fmt.print_ct_tree i; print_string "+- "; (* Print element *) - print_string ((type_name expr) ^ ": " ^ (type_string expr) ^ "\n") + print_string ((type_string expr) ^ "\n") ) in - let elexp_trace = print_trace elexp_name elexp_string elexp_location in + let elexp_trace = print_trace Elexp.to_string Elexp.location in (* Print the trace*) print_string (Fmt.make_title title); @@ -745,7 +741,7 @@ let int_to_string loc _depth args_val = match args_val with | _ -> error loc "Int->String expects one Int argument" let integer_to_string loc _depth args_val = match args_val with - | [Vinteger x] -> Vstring (BI.to_string x) + | [Vinteger x] -> Vstring (Z.to_string x) | _ -> error loc "Integer->String expects one Integer argument" let sys_exit loc _depth args_val = match args_val with @@ -818,7 +814,7 @@ let erasable_p name nth ectx = | (Some args) -> if (nth < (List.length args) && nth >= 0) then ( match (List.nth args nth) with - | (k, _, _) -> k = Aerasable ) + | (k, _, _) -> k = Pexp.Aerasable ) else false | _ -> false in try let idx = senv_lookup name ectx in @@ -838,7 +834,7 @@ let erasable_p2 t name ectx = -> (List.exists (fun (k, oname, _) -> match oname with - | (_, Some n) -> (n = name && k = Aerasable) + | (_, Some n) -> (n = name && k = Pexp.Aerasable) | _ -> false) args) | _ -> false in ===================================== src/fmt.ml ===================================== @@ -70,12 +70,14 @@ let print_ct_tree i = let red_f : _ format6 = "\x1b[31m" let green_f : _ format6 = "\x1b[32m" let yellow_f : _ format6 = "\x1b[33m" +let blue_f : _ format6 = "\x1b[34m" let magenta_f : _ format6 = "\x1b[35m" let cyan_f : _ format6 = "\x1b[36m" let reset_f : _ format6 = "\x1b[0m" let red = string_of_format red_f let green = string_of_format green_f +let blue = string_of_format blue_f let yellow = string_of_format yellow_f let magenta = string_of_format magenta_f let cyan = string_of_format cyan_f @@ -83,3 +85,39 @@ let reset = string_of_format reset_f let color_string color str = color ^ str ^ reset + +let formatter_of_out_channel (chan : out_channel) : Format.formatter = + let open Format in + let f = formatter_of_out_channel chan in + let isatty = chan |> Unix.descr_of_out_channel |> Unix.isatty in + let stag_fns : formatter_stag_functions = + { + mark_open_stag = + if isatty + then + function + | String_tag ("red") -> red + | String_tag ("green") -> green + | String_tag ("yellow") -> yellow + | String_tag ("blue") -> blue + | String_tag ("magenta") -> magenta + | String_tag ("cyan") -> cyan + | _ -> "" + else + Fun.const ""; + mark_close_stag = + if isatty + then + function + | String_tag ("red" | "green" | "yellow" | "blue" | "magenta" | "cyan") + -> reset + | _ -> "" + else + Fun.const ""; + print_open_stag = Fun.const (); + print_close_stag = Fun.const (); + } + in + Format.pp_set_formatter_stag_functions f stag_fns; + Format.pp_set_tags f true; + f ===================================== src/gambit.ml ===================================== @@ -18,13 +18,11 @@ * 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 Printf - open Debruijn open Elexp - -type ldecls = Lexp.ldecls -type lexp = Lexp.lexp +open Lexp +open Printf +open Sexp let gsc_path : string ref = ref "/usr/local/Gambit/bin/gsc" @@ -118,7 +116,7 @@ module Scm = struct match l, r with | Symbol l, Symbol r | String l, String r -> String.equal l r - | List ls, List rs -> Listx.equal equal ls rs + | List ls, List rs -> List.equal equal ls rs | Integer l, Integer r -> Z.equal l r | Float l, Float r -> Float.equal l r | _ -> false @@ -282,7 +280,9 @@ let rec scheme_of_expr (sctx : ScmContext.t) (elexp : elexp) : Scm.t = | Elexp.Type _ -> Scm.Symbol "lets-hope-its-ok-if-i-erase-this" - | _ -> failwith ("[gambit] unsupported elexp: " ^ elexp_string elexp) + | _ + -> failwith + (Format.asprintf "[gambit] unsupported elexp: %a" Elexp.pp_print elexp) class inferior script_path = let down_reader, down_writer = Unix.pipe ~cloexec:true () in ===================================== src/instargs.ml ===================================== @@ -112,9 +112,17 @@ let try_match t1 t2 lctx sl = | constraints when has_impossible constraints -> Impossible | _ -> Possible -let search_instance (instantiate_implicit) (ctx : DB.elab_context) - (loc : sinfo) (t : L.ltype) : L.lexp option = - Log.log_debug ~loc:(sexp_location loc) "Resolving type `%s`" (L.lexp_string t); +let search_instance + (instantiate_implicit) + (ctx : DB.elab_context) + (sinfo : sinfo) + (t : L.ltype) + : L.lexp option = + + Log.log_debug + ~loc:(Sexp.location sinfo) + "Resolving type `%s`" + (Lexp.to_string t); let lctx = DB.ectx_to_lctx ctx in let (_, _, insts) = DB.ectx_to_tcctx ctx in @@ -131,12 +139,12 @@ let search_instance (instantiate_implicit) (ctx : DB.elab_context) let env_elem_match (i, elem : U.db_index * DB.env_elem) : (int * DB.env_elem * L.lexp) option = let ((_, namopt), _, t') = elem in - let var = L.mkVar ((loc,namopt), i) in + let var = L.mkVar ((sinfo, namopt), i) in let t' = L.mkSusp t' (S.shift (i + 1)) in let (e, t') = instantiate_implicit var t' ctx in - Log.log_debug ~loc:(sexp_location loc) + Log.log_debug ~loc:(Sexp.location sinfo) "Considering potential instance `%s : %s` while resolving for `%s`" - (L.lexp_string var) (L.lexp_string t') (L.lexp_string t); + (Lexp.to_string var) (Lexp.to_string t') (Lexp.to_string t); (* All candidates should have a type that is a typeclass. *) if not (is_typeclass ctx t') then None else (* `try_match` uses the matching mode of unification where only @@ -150,10 +158,10 @@ let search_instance (instantiate_implicit) (ctx : DB.elab_context) | Possible -> (match !log_skipped_uncertain_matches with | Some level -> - Log.log_msg ignore level ~loc:(sexp_location loc) + Log.log_msg ignore level ~loc:(Sexp.location sinfo) "Skipping potential instance `%s : %s` while resolving for `%s`" - (L.lexp_string var) (L.lexp_string t') - (L.lexp_string t) + (Lexp.to_string var) (Lexp.to_string t') + (Lexp.to_string t) | None -> ()); None | Match -> Some (i, elem, e) in @@ -162,13 +170,13 @@ let search_instance (instantiate_implicit) (ctx : DB.elab_context) |> Seq.filter_map env_elem_match in if !debug_list_all_candidates then - Log.log_debug "Candidates for instance of type `%s`:" (L.lexp_string t) + Log.log_debug "Candidates for instance of type `%s`:" (Lexp.to_string t) ~print_action:(fun () -> Seq.iter (fun (i, ((_, so),_,t'), _) -> printf "%-4i %-10s %s\n" i (* De Bruijn index *) (match so with | Some s -> s | None -> "<none>") (* Var name *) - (L.lexp_string t') (* Variable type *) + (Lexp.to_string t') (* Variable type *) ) candidates); let inst = match candidates () with @@ -179,10 +187,10 @@ let search_instance (instantiate_implicit) (ctx : DB.elab_context) | None -> None | Some (i, (vname, _, t'), e) -> let t' = L.mkSusp t' (S.shift (i + 1)) in - Log.log_debug ~loc:(sexp_location loc) + Log.log_debug ~loc:(Sexp.location sinfo) "Found instance for `%s` at index %i: `%s : %s`" - (L.lexp_string t) i - (L.lexp_string (L.mkVar (vname, i))) (L.lexp_string t'); + (Lexp.to_string t) i + (Lexp.to_string (L.mkVar (vname, i))) (Lexp.to_string t'); Some e let resolve_instances instantiate_implicit e = @@ -191,7 +199,7 @@ let resolve_instances instantiate_implicit e = let changed = (U.IMap.fold (fun i (_sl, t, _cl, _vn) changed -> (match lookup_metavar_resolution_ctxt i with - | Some (ctx, loc) -> + | Some (ctx, sinfo) -> (* Start by the instance metavars in the type: no need to decrement the recursion limit here. *) resolve_instances t limit; @@ -199,15 +207,18 @@ let resolve_instances instantiate_implicit e = match L.metavar_lookup i with | MVar _ -> true | _ -> false in - if uninstantiated && is_typeclass ctx t then - (match search_instance instantiate_implicit ctx (loc) t with + if uninstantiated && is_typeclass ctx t + then + (match search_instance instantiate_implicit ctx sinfo t with | Some e -> Unif.associate i e; true - | None -> - (* The metavar will be generalized, unified, or - will remain and cause an error. *) - Log.log_info ~loc:(sexp_location loc) "No instance found for type `%s`" - (L.lexp_string t); false - ) + + (* The metavar will be generalized, unified, or will remain + and cause an error. *) + | None + -> Log.log_info + ~loc:(Sexp.location sinfo) "No instance found for type `%s`" + (Lexp.to_string t); + false) else false | None -> false ) || changed) fv_map false) in @@ -217,7 +228,7 @@ let resolve_instances instantiate_implicit e = resolve_instances e (Some (l - 1)) | None -> resolve_instances e None | _ -> - Log.log_error ~loc:(L.lexp_location e) + Log.log_error ~loc:(Lexp.location e) "Instance resolution recursion limit reached in expression : `%s`" - (L.lexp_string e) in + (Lexp.to_string e) in resolve_instances e !recursion_limit ===================================== src/inverse_subst.ml ===================================== @@ -174,11 +174,17 @@ let inverse (s: subst) : subst option = -> if is_identity (Lexp.scompose s s1) || is_identity (Lexp.scompose s1 s) then () else - Log.log_debug - "Subst-inversion-bug: %s ∘ %s == %s !!\n" - (subst_string s) - (subst_string s1) - (subst_string (Lexp.scompose s1 s)) + let message = + Format.asprintf + "Subst-inversion-bug: %a ∘ %a == %a !!\n" + Lexp.pp_print_subst + s + Lexp.pp_print_subst + s1 + Lexp.pp_print_subst + (Lexp.scompose s1 s) + in + Log.log_debug "%s" message | _ -> ()); res ===================================== src/lexer.ml ===================================== @@ -149,9 +149,9 @@ let lex_symbol in let location s = s - |> sexp_location + |> Sexp.location |> Source.Location.extend op_location - |> Source.Location.extend (sexp_location left) + |> Source.Location.extend (Sexp.location left) in let lf' = if prec' > prec ===================================== src/lexp.ml ===================================== @@ -1,6 +1,6 @@ (* lexp.ml --- Lambda-expressions: the core language. -Copyright (C) 2011-2022 Free Software Foundation, Inc. +Copyright (C) 2011-2023 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> Keywords: languages, lisp, dependent types. @@ -20,28 +20,17 @@ 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/>. *) -module U = Util -module L = List -module SMap = U.SMap -open Fmt - -open Sexp open Pexp +open Sexp -open Grammar - -(* open Unify *) +module L = List module S = Subst +module SMap = Util.SMap +module U = Util -type vname = Sexp.vname -type vref = Sexp.vref type meta_id = int (* Identifier of a meta variable. *) -type sinfo = sexp - type label = symbol -include Pexp.ArgKind - (*************** Elaboration to Lexp *********************) (* The scoping of `Let` is tricky: @@ -336,7 +325,7 @@ let impossible = mkImm Sexp.dummy_epsilon let lexp_head e = match lexp_lexp' e with | Imm s -> - if e = impossible then "impossible" else "Imm" ^ sexp_string s + if e = impossible then "impossible" else "Imm" ^ Sexp.to_string s | Var _ -> "Var" | Proj _ -> "Proj" | Let _ -> "let" @@ -537,15 +526,15 @@ let rec lexp_sinfo s = | Metavar (_,_,(l,_)) -> l | Proj (l,_,_) -> l - -let lexp_location (e : lexp) : Source.Location.t = - e |> lexp_sinfo |> sexp_location +let location (e : lexp) : Source.Location.t = + Sexp.location (lexp_sinfo e) (********* Normalizing a term *********) let vdummy = (dummy_sinfo, None) let maybename n = match n with None -> "<anon>" | Some v -> v -let sname (l,n) = (sexp_location l, maybename n) +let sname (sinfo, n : vname) : symbol = + (Sexp.location sinfo, maybename n) let rec push_susp e s = (* Push a suspension one level down. *) match lexp_lexp' e with @@ -677,511 +666,328 @@ let clean e = | _ -> mkMetavar (idx, s, name) in clean S.identity e -let sdatacons = Symbol (U.dummy_location, "##datacons") -let stypecons = Symbol (U.dummy_location, "##typecons") - -(* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) -let rec lexp_unparse lxp = - match lexp_lexp' lxp with - | Susp _ -> lexp_unparse (nosusp lxp) - | Imm (sexp) -> sexp - | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) - (* FIXME: Add a Sexp syntax for debindex references. *) - | Var ((loc, name), _) -> Symbol (sexp_location loc, maybename name) - | Proj (sinfo, lxp, (loc, str)) - -> let location = sexp_location sinfo in - Node (location, - Symbol (location, "__.__"), - [(lexp_unparse lxp); (Symbol (loc, str))]) - | Cons (t, (l, name)) - -> Node (l, sdatacons, [lexp_unparse t; Symbol (l, name)]) - | Lambda (kind, vdef, ltp, body) - -> let l = lexp_location lxp in - let st = lexp_unparse ltp in - Node (l, - Symbol (l, match kind with - | Anormal -> "lambda_->_" - | Aimplicit -> "lambda_=>_" - | Aerasable -> "lambda_≡>_"), - [Node (l, Symbol (l, "_:_"), [Symbol (sname vdef); st]); - lexp_unparse body]) - - | Arrow (sinfo, arg_kind, (sinfo_v, oname), ltp1, ltp2) - -> let location = sexp_location sinfo in - let location_v = sexp_location sinfo_v in - let ut1 = lexp_unparse ltp1 in - Node (location, - Symbol (location, - match arg_kind with Anormal -> "_->_" - | Aimplicit -> "_=>_" - | Aerasable -> "_≡>_"), - [(match oname with - | None -> ut1 - | Some v -> Node (location, - Symbol (location_v, "_:_"), - [Symbol (location_v, v); ut1])); - lexp_unparse ltp2]) - - | Let (sinfo, ldecls, body) (* (vdef * lexp * ltype) list *) - -> let location = sexp_location sinfo in - let sdecls = List.fold_left - (fun acc (vdef, lxp, ltp) - -> Node (location, - Symbol (U.dummy_location, "_=_"), - [Symbol (sname vdef); lexp_unparse ltp]) - :: Node (location, - Symbol (U.dummy_location, "_=_"), - [Symbol (sname vdef); lexp_unparse lxp]) - :: acc) - [] ldecls in - Node (location, - Symbol (location, "let_in_"), - [Node (location, Symbol (U.dummy_location, "_;_"), sdecls); - lexp_unparse body]) - - - | Call (sinfo, lxp, largs) (* (arg_kind * lexp) list *) - -> let sargs = List.map (fun (_kind, elem) -> lexp_unparse elem) largs in - Node (sexp_location sinfo, lexp_unparse lxp, sargs) - - (* (arg_kind * vdef * ltype) list *) - (* (arg_kind * pvar * pexp option) list *) - | Inductive (sinfo, label, lfargs, ctors) - -> let location = sexp_location sinfo in - let pfargs = - List.map - (fun (kind, vdef, ltp) - -> (kind, sname vdef, Some (lexp_unparse ltp))) - lfargs - in - Node (location, - stypecons, - Node (location, Symbol label, List.map pexp_u_formal_arg pfargs) - :: List.map - (fun (name, types) - -> Node (location, - Sexp.symbol ~location name, - List.map - (fun arg -> - match arg with - | (Anormal, (_, None), t) -> lexp_unparse t - | (ak, s, t) - -> let (l, _) as id = sname s in - Node (location, - Symbol (l, match ak with - | Anormal -> "_:_" - | Aimplicit -> "_::_" - | Aerasable -> "_:::_"), - [Symbol id; lexp_unparse t])) - types)) - (SMap.bindings ctors)) - - | Case (sinfo, target, bltp, branches, default) - -> let bt = lexp_unparse bltp in - let unparse_pbranch (str, (sinfo, args, bch)) = - let location = sexp_location sinfo in - match args with - | [] -> Ppatsym (sinfo, Some str), lexp_unparse bch - | _ -> - let pat_args - = List.map (fun (_kind, ((sinfo, oname) as name)) - -> let location = sexp_location sinfo in - match oname with - | Some vdef -> (Some (location, vdef), name) - | None -> (None, name)) - args - (* FIXME: Rather than a Pcons we'd like to refer to an existing - * binding with that value! *) - in - let pattern = - Ppatcons (location, - Node (location, - sdatacons, - [bt; Symbol (location, str)]), - pat_args) - in - (pattern, lexp_unparse bch) - in - let pbranch = List.map unparse_pbranch (SMap.bindings branches) in - - let pbranch = match default with - | Some (v,dft) -> (Ppatsym v, lexp_unparse dft) :: pbranch - | None -> pbranch - in - let e = lexp_unparse target in - let location = sexp_location sinfo in - Node (location, - Symbol (location, "case_"), - e :: List.map - (fun (pat, branch) -> - Node (location, - Symbol (pexp_pat_location pat, "_=>_"), - [pexp_u_pat pat; branch])) - pbranch) - - (* FIXME: The cases below are all broken! *) - | Metavar (idx, subst, (sinfo, name)) - -> Symbol (sexp_location sinfo, "?" ^ (maybename name) ^ "-" ^ string_of_int idx - ^ "[" ^ subst_string subst ^ "]") - - | SortLevel (SLz) -> Symbol (U.dummy_location, "##TypeLevel.z") - - | SortLevel (SLsucc l) - -> let location = lexp_location l in - Node (location, Symbol (location, "##TypeLevel.succ"), [lexp_unparse l]) - - | SortLevel (SLlub (l1, l2)) - -> let location = - Source.Location.extend (lexp_location l1) (lexp_location l2) - in - Node (location, - Symbol (lexp_location l1, "##TypeLevel.∪"), - [lexp_unparse l1; lexp_unparse l2]) - - | Sort (l, StypeOmega) -> Symbol (sexp_location l, "##Type_ω") - - | Sort (l, StypeLevel) -> Symbol (sexp_location l, "##TypeLevel.Sort") - - | Sort (l, Stype sl) - -> Node (sexp_location l, - Symbol (lexp_location sl, "##Type_"), - [lexp_unparse sl]) - -(* FIXME: ¡Unify lexp_print and lexp_string! *) -and lexp_string lxp = sexp_string (lexp_unparse lxp) - -and subst_string s = match s with - | S.Identity o -> "↑" ^ string_of_int o - | S.Cons (l, s, 0) -> lexp_name l ^ " · " ^ subst_string s - | S.Cons (l, s, o) - -> "(↑"^ string_of_int o ^ " " ^ subst_string (S.cons l s) ^ ")" - -and lexp_name e = - match lexp_lexp' e with - | Imm _ -> lexp_string e - | Var _ -> lexp_string e - | _ -> lexp_head e - -(* ------------------------------------------------------------------------- *) -(* Printing *) - -(* Printing Context - * ========================================== *) - -type print_context_value = - | Bool of bool - | Int of int - | Predtl of Grammar.t (** precedence table *) - -type print_context = print_context_value SMap.t - -let pretty_ppctx = - List.fold_left (fun map (key, v) -> SMap.add key v map) - SMap.empty - [("pretty" , Bool (true) ); (* print with new lines and indents *) - ("print_type" , Bool (true) ); (* print inferred Type *) - ("print_dbi" , Bool (false)); (* print dbi index *) - ("indent_size" , Int (2) ); (* indent step *) - ("color" , Bool (true) ); (* use console color to display hints *) - ("separate_decl" , Bool (true) ); (* print newline between declarations *) - ("indent_level" , Int (0) ); (* current indent level *) - ("col_max" , Int (80) ); (* col_size + col_ofsset <= col_max *) - ("col_size" , Int (0) ); (* current column size *) - ("col_ofsset" , Int (0) ); (* if col does not start at 0 *) - ("print_erasable", Bool (false)); - ("print_implicit", Bool (false)); - ("grammar" , Predtl (default_grammar))] - -(* debug_ppctx is a ref so we can modify it in the REPL *) -let debug_ppctx = ref ( - List.fold_left (fun map (key, v) -> SMap.add key v map) - pretty_ppctx - [("pretty" , Bool (false) ); - ("print_dbi" , Bool (true) ); - ("print_erasable", Bool (true)); - ("print_implicit", Bool (true)); - ("separate_decl" , Bool (false) );]) - -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_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_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 -let reset_col_size ctx = set_col_size 0 ctx -let add_indent ctx i = SMap.add "indent_level" (Int ((pp_indent ctx) + i)) ctx - -let pp_append_string buffer ctx str = - let n = (String.length str) in - Buffer.add_string buffer str; - add_col_size n ctx -let pp_newline buffer ctx = - Buffer.add_char buffer '\n'; - reset_col_size ctx - -let is_binary_op str = - let len = String.length str in - let c1 = String.get str 0 in - let cn = String.get str (len - 1) in - if (c1 = '_') && (cn = '_') && (len > 2) then true else false - -let get_binary_op_name name = - assert (((String.length name) - 2) >= 1); - String.sub name 1 ((String.length name) - 2) - -let rec get_precedence expr ctx = - let lkp name = Grammar.find name (pp_grammar ctx) in - match lexp_lexp' expr with - | Lambda _ -> lkp "lambda" - | Case _ -> lkp "case" - | Let _ -> lkp "let" - | Arrow (_, Anormal, _, _, _) -> lkp "->" - | Arrow (_, Aimplicit, _, _, _) -> lkp "=>" - | Arrow (_, Aerasable, _, _, _) -> lkp "≡>" - | Call (_, exp, _) -> get_precedence exp ctx - | Builtin ((_, name), _) when is_binary_op name -> - lkp (get_binary_op_name name) - | Var ((_, Some name), _) when is_binary_op name -> - lkp (get_binary_op_name name) - | _ -> None, None - -(* Printing Functions - * ========================================== *) - -let rec lexp_print e = print_string (lexp_string e) -and lexp_string e = lexp_cstring (!debug_ppctx) e - -(* Context Print *) -and lexp_cprint ctx e = print_string (lexp_cstring ctx e) -and lexp_cstring ctx e = lexp_str ctx e - -(* Implementation *) -and lexp_str ctx (exp : lexp) : string = - - let inter_ctx = add_indent ctx 1 in - let lexp_str' = lexp_str ctx in - let lexp_stri idt e = lexp_str (add_indent ctx idt) e in - - let pretty = pp_pretty ctx in - let color = pp_color ctx in - let indent = pp_indent ctx in - let isize = pp_size ctx in - - (* colors *) - let red = if color then red else "" in - let green = if color then green else "" in - let yellow = if color then yellow else "" in - let magenta = if color then magenta else "" in - let cyan = if color then cyan else "" in - let reset = if color then reset else "" in - - let make_indent idt = if pretty then - (make_line ' ' ((idt + indent) * isize)) else "" in - - let newline = if pretty then "\n" else " " in - let nl = newline in - - let keyword str = magenta ^ str ^ reset in - let error str = red ^ str ^ reset in - let tval str = yellow ^ str ^ reset in - let fun_call str = cyan ^ str ^ reset in - - let index idx = - let str = if pp_dbi ctx - then ("[" ^ (string_of_int idx) ^ "]") - else "" in - if idx < 0 then error str - else green ^ str ^ reset in - - let kind_str k = match k with - | Anormal -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>" in - - let kindp_str k = match k with - | Anormal -> ":" | Aimplicit -> "::" | Aerasable -> ":::" in - - let get_name fname = - match lexp_lexp' fname with - | Builtin ((_, name), _) -> name, 0 - | Var((_, Some name), idx) -> name, idx - | Lambda _ -> "__", 0 - | Cons _ -> "__", 0 - | _ -> "__", -1 in - - match lexp_lexp' exp with - | Imm(value) -> (match value with - | String (_, s) -> tval ("\"" ^ s ^ "\"") - | Integer(_, s) -> tval (Z.to_string s) - | Float (_, s) -> tval (string_of_float s) - | e -> sexp_string e) - - | Susp (e, s) -> lexp_str ctx (push_susp e s) - - | Var ((_loc, name), idx) -> maybename name ^ (index idx) ; - - | Proj (_, lxp, (_, str)) - -> "( __.__ " ^ lexp_str' lxp ^ " " ^ str ^ " )" - - | Metavar (idx, subst, (_loc, name)) - (* print metavar result if any *) - -> (match metavar_lookup idx with - | MVal e -> lexp_str ctx (push_susp e subst) - | _ -> "?" ^ maybename name ^ (subst_string subst) ^ (index idx)) - - | Let (_, decls, body) -> - (* Print first decls without indent *) - let h1, decls, idt_lvl = - match lexp_str_decls inter_ctx decls with - | h1::decls -> h1, decls, 2 - | _ -> "", [], 1 in - - let decls = List.fold_left (fun str elem -> - str ^ nl ^ (make_indent 1) ^ elem ^ " ") h1 decls in - - let n = String.length decls in - (* remove last newline *) - let decls = if (n > 0) then - String.sub decls 0 (n - 2) - else decls in - - (keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^ - (make_indent idt_lvl) ^ (lexp_stri idt_lvl body) - - | Arrow(_loc, k, (_, Some name), tp, expr) -> - "(" ^ name ^ " : " ^ (lexp_str' tp) ^ ") " ^ - (kind_str k) ^ " " ^ (lexp_str' expr) - - | Arrow(_loc, k, (_, None), tp, expr) -> - "(" ^ (lexp_str' tp) ^ " " - ^ (kind_str k) ^ " " ^ (lexp_str' expr) ^ ")" - - | Lambda(k, (_loc, name), ltype, lbody) -> - let arg = "(" ^ maybename name ^ " : " ^ (lexp_str' ltype) ^ ")" in - - (keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^ - (make_indent 1) ^ (lexp_stri 1 lbody) - - | Cons(t, (_, ctor_name)) -> - (keyword "datacons ") ^ (lexp_str' t) ^ " " ^ ctor_name - - | Call(_, fname, args) -> - let name, idx = get_name fname in - let binop_str op (_, lhs) (_, rhs) = - "(" ^ (lexp_str' lhs) ^ op ^ (index idx) ^ " " ^ (lexp_str' rhs) ^ ")" in - - let print_arg str (arg_type, lxp) = - match arg_type with - | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str' lxp) - | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str' lxp) - | Anormal -> str ^ " " ^ (lexp_str' lxp) - | _ -> str in ( - - match args with - | [lhs; rhs] when is_binary_op name -> - binop_str (" " ^ (get_binary_op_name name)) lhs rhs - - | _ -> let args = List.fold_left print_arg "" args in - "(" ^ (lexp_str' fname) ^ args ^ ")") - - | Inductive (_, (_, name), [], ctors) -> - (keyword "typecons") ^ " (" ^ name ^") " ^ newline ^ - (lexp_str_ctor ctx ctors) - - | Inductive (_, (_, name), args, ctors) - -> let args_str - = List.fold_left - (fun str (arg_kind, (_, name), ltype) - -> str ^ " (" ^ maybename name ^ " " ^ (kindp_str arg_kind) ^ " " - ^ (lexp_str' ltype) ^ ")") - "" args in - - (keyword "typecons") ^ " (" ^ name ^ args_str ^") " ^ - (lexp_str_ctor ctx ctors) - - | Case (_, target, _ret, map, dflt) ->( - let str = (keyword "case ") ^ (lexp_str' target) in - let arg_str arg - = List.fold_left (fun str v - -> match v with - | (_, (_, None)) -> str ^ " _" - | (_, (_, Some n)) -> str ^ " " ^ n) - "" arg in - - let str = SMap.fold (fun k (_, arg, exp) str -> - str ^ nl ^ (make_indent 1) ^ - "| " ^ (fun_call k) ^ (arg_str arg) ^ " => " ^ (lexp_stri 1 exp)) - map str in - - match dflt with - | None -> str - | Some (v, df) -> - str ^ nl ^ (make_indent 1) - ^ "| " ^ (match v with (_, None) -> "_" - | (_, Some name) -> name) - ^ " => " ^ (lexp_stri 1 df)) - - | Builtin ((_, name), _) -> "##" ^ name - - | Sort (_, StypeLevel) -> "##TypeLevel.Sort" - | Sort (_, StypeOmega) -> "##Type_ω" - - | SortLevel (SLz) -> "##TypeLevel.z" - | SortLevel (SLsucc e) -> "(##TypeLevel.succ " ^ lexp_string e ^ ")" - | SortLevel (SLlub (e1, e2)) - -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e2 ^ ")" - - | Sort (_, Stype l) - -> match lexp_lexp' l with - | SortLevel SLz -> "##Type" - | SortLevel (SLsucc lp) - when (match lexp_lexp' lp with SortLevel SLz -> true | _ -> false) - -> "##Type1" - | _ -> "(##Type_ " ^ lexp_string l ^ ")" - -and lexp_str_ctor ctx ctors = - - let pretty = pp_pretty ctx in - let make_indent idt = if pretty then (make_line ' ' ((idt + (pp_indent ctx)) * (pp_size ctx))) else "" in - let newline = (if pretty then "\n" else " ") in - - SMap.fold (fun key value str - -> let str = str ^ newline ^ (make_indent 1) ^ "(" ^ key in - let str = List.fold_left (fun str (_k, _, arg) - -> str ^ " " ^ (lexp_str ctx arg)) - str value in - str ^ ")") - ctors "" - -and lexp_str_decls ctx decls = - - let lexp_str' = lexp_str ctx in - let sepdecl = (if pp_decl ctx then "\n" else "") in - - let type_str name lxp = (if pp_type ctx then ( - name ^ " : " ^ (lexp_str' lxp) ^ ";") else "") in - - let ret = List.fold_left - (fun str ((_, name), lxp, ltp) - -> let name = maybename name in - let str = if pp_type ctx then (type_str name ltp)::str else str in - (name ^ " = " ^ (lexp_str' lxp) ^ ";" ^ sepdecl)::str) - [] decls in - List.rev ret +type Format.stag += Indexed of int + +let pp_enable_print_indices (f : Format.formatter) : unit = + let fns = Format.pp_get_formatter_stag_functions f () in + let fns' = + { + fns with + print_open_stag = + begin function + | Indexed _ -> () + | stag -> fns.print_open_stag stag + end; + print_close_stag = + begin function + | Indexed (index) -> Format.fprintf f "@{<green>[%d]@}" index + | stag -> fns.print_close_stag stag + end; + } + in + Format.pp_set_formatter_stag_functions f fns'; + Format.pp_set_tags f true + +let pp_print_var (f : Format.formatter) (name : vname) (index : int) : unit = + let open Format in + pp_open_stag f (Indexed (index)); + pp_print_string f (string_of_vname name); + pp_close_stag f () + +let pp_print_proj + (type expr field) + (f : Format.formatter) + (pp_print_expr : Format.formatter -> expr -> unit) + (e : expr) + (pp_print_field : Format.formatter -> field -> unit) + (field_name : field) + : unit = + Format.fprintf + f + "@[<hov 1>(__.__@ (%a)@ %a)@]" + pp_print_expr + e + pp_print_field + field_name + +let pp_print_builtin (f : Format.formatter) (name : Sexp.symbol) : unit = + Format.fprintf f "##%a" Sym.pp_print name + +let pp_print_let + (type decls expr) + (f : Format.formatter) + (pp_print_decl_block : Format.formatter -> decls -> unit) + (decls : decls) + (pp_print_body : Format.formatter -> expr -> unit) + (body : expr) + : unit = + Format.fprintf + f + "@[<v>@[<v 2>@{<magenta>let@}@;%a@]@;@[<v 2>@{<magenta>in@}@;%a;@]@]" + pp_print_decl_block + decls + pp_print_body + body + +let pp_print_call + (type expr arg) + (f : Format.formatter) + (pp_print_callee : Format.formatter -> expr -> unit) + (callee : expr) + (pp_print_arg : Format.formatter -> arg -> unit) + (args : arg list) + : unit = + let open Format in + fprintf f "@[<hov 1>(%a" pp_print_callee callee; + List.iter (fun arg -> fprintf f "@ %a" pp_print_arg arg) args; + fprintf f ")@]" + +let pp_print_lambda + (type expr param) + (f : Format.formatter) + (pp_print_param : Format.formatter -> param -> unit) + (param : param) + (param_kind : ArgKind.t) + (pp_print_body : Format.formatter -> expr -> unit) + (body : expr) + : unit = + Format.fprintf + f + "@[<v 1>(@{<magenta>lambda@} %a %s@;%a)@]" + pp_print_param + param + (ArgKind.to_arrow param_kind) + pp_print_body + body + +let pp_print_case + (type meta expr binding) + (f : Format.formatter) + (pp_print_expr : Format.formatter -> expr -> unit) + (e : expr) + (pp_print_binding : Format.formatter -> binding -> unit) + (branches : (meta * binding list * expr) SMap.t) + (default : (vname * expr) option) + : unit = + + let open Format in + let pp_print_branch f cons_name (_, args, body) = + fprintf + f + "@ @[<hov 2>| %s@ @[<hov 1>%a@] ->@ %a@]" + cons_name + (pp_print_list ~pp_sep:pp_print_space pp_print_binding) + args + pp_print_expr + body + in + let pp_print_branches f branches = + SMap.iter (pp_print_branch f) branches + in + let pp_print_default f branch = + match branch with + | None -> () + | Some ((binding, body)) + -> fprintf + f + "@ @[<hov 2>| %s ->@ %a@]" + (Sexp.string_of_vname binding) + pp_print_expr + body + in + fprintf + f + "@[<v 1>(@[<hov 2>@{<magenta>case@}@ %a@]%a%a)@]" + pp_print_expr + e + pp_print_branches + branches + pp_print_default + default + +let rec pp_print (f : Format.formatter) (e, _ : lexp) : unit = + let open Format in + match e with + | Imm (v) + -> Sexp.pp_print f v + + | Susp (e, s) + -> pp_print f (push_susp e s) + + | Builtin (name, _) + -> pp_print_builtin f name + + | Var ((name, index)) + -> pp_print_var f name index + + | Metavar (index, subst, name) + -> begin match metavar_lookup index with + | MVal e -> pp_print f (push_susp e subst) + | _ + -> pp_open_stag f (Indexed (index)); + fprintf f "?%s%a" (string_of_vname name) pp_print_subst subst; + pp_close_stag f () + end + + | Proj (_, e, field_name) + -> pp_print_proj f pp_print e Sym.pp_print field_name + + | Cons (e, (_, cons_name)) + -> fprintf + f + "@[<hov 1>(@{<magenta>datacons@}@ %a@ %s)@]" + pp_print + e + cons_name + + | Lambda (kind, param_name, param_ty, body) + -> pp_print_lambda + f + (fun f (param_name, param_ty) + -> fprintf + f + "@[<hov 2>(%s@ : %a)@]" + (Sexp.string_of_vname param_name) + pp_print + param_ty) + (param_name, param_ty) + kind + pp_print + body + + | Arrow (_, kind, (_, None), arg_ty, body_ty) + -> fprintf + f + "@[<hov 2>(%a@ %s %a)@]" + pp_print + arg_ty + (ArgKind.to_arrow kind) + pp_print + body_ty + + | Arrow (_, kind, (_, Some (name)), arg_ty, body_ty) + -> fprintf + f + "@[<hov 2>(%s@ : %a@ %s %a)@]" + name + pp_print + arg_ty + (ArgKind.to_arrow kind) + pp_print + body_ty + + | Let (_, decls, body) + -> pp_print_let f pp_print_decl_block decls pp_print body + + | Call (_, callee, args) + -> pp_print_call f pp_print callee (fun f (_, arg) -> pp_print f arg) args + + | Inductive (_, name, params, constructors) + -> let pp_print_param f (kind, name, ty) = + match kind, name with + | Anormal, (_, None) -> fprintf f "@ @[<hov 1>(%a)@]" pp_print ty + | _, _ + -> fprintf + f + "@ @[<hov 1>(%s %s@ %a)@]" + (Sexp.string_of_vname name) + (ArgKind.to_colon kind) + pp_print + ty + in + let pp_print_params f params = + List.iter (pp_print_param f) params + in + let pp_print_cons name params = + fprintf f "@ @[<hov 1>(%s%a)@]" name pp_print_params params + in + + fprintf f "@[<hov 1>(@{<magenta>typecons@} "; + begin match params with + | [] -> Sym.pp_print f name + | _ :: _ + -> fprintf + f + "@[<hov 1>(%a%a)@]" + Sym.pp_print + name + pp_print_params + params + end; + SMap.iter pp_print_cons constructors + + | Case (_, e, _, branches, default) + -> let pp_print_binding f (_, name) = + pp_print_string f (Sexp.string_of_vname ~default:"_" name) + in + pp_print_case f pp_print e pp_print_binding branches default + + | Sort (_, sort) + -> pp_print_sort f sort + + | SortLevel ( sort_level) + -> pp_print_sort_level f sort_level + +and pp_print_subst (f : Format.formatter) (subst : subst) : unit = + let open Format in + match subst with + | Subst.Identity (o) + -> fprintf f "↑%d" o + | Subst.Cons (l, s, 0) + -> fprintf f "(%a) · %a" pp_print l pp_print_subst s + | Subst.Cons (l, s, o) + -> fprintf f "(↑%d %a)" o pp_print_subst (Subst.cons l s) + +and pp_print_sort (f : Format.formatter) (sort : sort) : unit = + let open Format in + match sort with + | StypeLevel -> pp_print_string f "##TypeLevel.Sort" + | StypeOmega -> pp_print_string f "##Type_ω" + | Stype ((SortLevel SLz, _)) -> pp_print_string f "##Type" + | Stype ((SortLevel (SLsucc (SortLevel SLz, _)), _)) + -> pp_print_string f "##Type1" + | Stype (e) + -> fprintf f "@[<hov 1>(##Type_@ %a)@]" pp_print e + +and pp_print_sort_level (f : Format.formatter) (level : sort_level) : unit = + let open Format in + match level with + | SLz -> pp_print_string f "##TypeLevel.z" + | SLsucc (e) -> fprintf f "@[<hov 1>(##TypeLevel.succ@ %a)@]" pp_print e + | SLlub (l, r) + -> fprintf f "@[<hov 1>(##TypeLevel.∪@ %a@ %a)@]" pp_print l pp_print r + +and pp_print_decl_block (f : Format.formatter) (ldecls : ldecls) : unit = + let open Format in + pp_open_vbox f 0; + pp_print_list + ~pp_sep:pp_print_space + (fun f (name, _, ty) + -> fprintf f "@[<hov 2>%s :@ %a;@]" (string_of_vname name) pp_print ty) + f + ldecls; + pp_print_cut f (); + pp_print_list + ~pp_sep:pp_print_space + (fun f (name, body, _) + -> fprintf f "@[<hov 2>%s =@ %a;@]" (string_of_vname name) pp_print body) + f + ldecls; + pp_close_box f () + +let pp_print_decls (f : Format.formatter) (ldecls : ldecls list) : unit = + let open Format in + fprintf + f + "@[<v 0>%a@]" + (pp_print_list ~pp_sep:pp_print_cut pp_print_decl_block) + ldecls + +let print : lexp -> unit = + Format.printf "%a" pp_print + +let to_string : lexp -> string = + Format.asprintf "%a" pp_print (** Syntactic equality (i.e. without β). *******) ===================================== src/listx.ml → src/list.ml ===================================== @@ -18,6 +18,8 @@ * 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 + (* Backport from 4.12. *) let rec equal (p : 'a -> 'a -> bool) (ls : 'a list) (rs : 'a list) : bool = match ls, rs with ===================================== src/opslexp.ml ===================================== @@ -204,9 +204,9 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = | Sort (_, Stype l) -> l | _ -> Log.internal_error "" in mkCall (l, DB.eq_refl, - [L.Aerasable, elevel; - L.Aerasable, etype; - L.Aerasable, e]) in + [Pexp.Aerasable, elevel; + Pexp.Aerasable, etype; + Pexp.Aerasable, e]) in let reduce it name aargs = let targs = match lexp'_whnf it ctx with | Inductive (_,_,fargs,_) -> fargs @@ -233,7 +233,7 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = -> let subst = S.cons (get_refl e') (S.substitute e') in lexp_whnf (push_susp default subst) ctx | _ -> Log.log_error - ~section:"WHNF" ~loc:(sexp_location l) + ~section:"WHNF" ~loc:(Sexp.location l) {|Unhandled constructor "%s" in case expression|} name; mkCase (l, e, rt, branches, default) in (match lexp_lexp' e' with @@ -259,17 +259,17 @@ let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = _ -> []) in let rec getfield label args fields = match args, fields with - | _ , [] -> Log.log_error ~loc:(sexp_location loc) + | _ , [] -> Log.log_error ~loc:(Sexp.location loc) "Tuple does not have the field `%s`" label; e | (_, arg)::_, (_, (_, Some fn), _)::_ when fn = label -> (* Reduce to the argument corresponding to the field *) lexp_whnf arg ctx | _::args, _::fields -> getfield label args fields | [], _ -> (* This case should be impossible through typing *) - Log.log_fatal ~loc:(sexp_location loc) + Log.log_fatal ~loc:(Sexp.location loc) "Projected tuple has fewer arguments than fields" in getfield label (drop (List.length targs) args) fields - | _ -> Log.log_error ~loc:(sexp_location loc) "Proj on a non-tuple in WHNF!"; e) + | _ -> Log.log_error ~loc:(Sexp.location loc) "Proj on a non-tuple in WHNF!"; e) | _ -> e) (* Not a proj of a cons: don't reduce. *) | Metavar (idx, s, _) @@ -441,7 +441,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let ekind = get_type ctx etype in let elvl = match lexp'_whnf ekind ctx with | Sort (_, Stype l) -> l - | _ -> Log.log_fatal ~loc:(lexp_location ekind) + | _ -> Log.log_fatal ~loc:(Lexp.location ekind) "Target lexp's kind is not a sort"; in (* 1. Get the inductive for the field types *) let it, aargs = match lexp_lexp' etype with @@ -461,10 +461,10 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in let eqty = mkCall (dsinfo, DB.type_eq, - [(L.Aerasable, tlvl); (* Typelevel *) - (L.Aerasable, tltp); (* Inductive type *) - (L.Anormal, hlxp); (* Lexp of the branch head *) - (L.Anormal, tlxp)]) in (* Target lexp *) + [(Pexp.Aerasable, tlvl); (* Typelevel *) + (Pexp.Aerasable, tltp); (* Inductive type *) + (Pexp.Anormal, hlxp); (* Lexp of the branch head *) + (Pexp.Anormal, tlxp)]) in (* Target lexp *) DB.lexp_ctx_cons ctx (dsinfo, None) Variable eqty in (* The map module doesn't have a function to compare two maps with the key (which is needed to get the field types @@ -553,9 +553,9 @@ and sort_compose ctx1 ctx2 l ak k1 k2 = -> if ak == P.Aerasable && impredicative_erase then SortResult (mkSusp k2 (S.substitute impossible)) else let l2' = (mkSusp l2 (S.substitute impossible)) in - (* print_string ("Normal: " ^ lexp_string l1 ^ " -> " - * ^ lexp_string l2' ^ " ==> " - * ^ lexp_string (mkSort (l, Stype (mkSLlub ctx1 l1 l2'))) + (* print_string ("Normal: " ^ Lexp.to_string l1 ^ " -> " + * ^ Lexp.to_string l2' ^ " ==> " + * ^ Lexp.to_string (mkSort (l, Stype (mkSLlub ctx1 l1 l2'))) * ^ "\n"); *) SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2'))) | (StypeLevel, Stype _l2) @@ -564,9 +564,9 @@ and sort_compose ctx1 ctx2 l ak k1 k2 = * 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. *) - -> (* print_string ("ImpUniv: " ^ lexp_string k1 ^ " ≡> " - * ^ lexp_string k2 ^ " ==> " - * ^ lexp_string (mkSusp k2 (S.substitute DB.level0)) + -> (* print_string ("ImpUniv: " ^ Lexp.to_string k1 ^ " ≡> " + * ^ Lexp.to_string k2 ^ " ==> " + * ^ Lexp.to_string (mkSusp k2 (S.substitute DB.level0)) * ^ "\n"); *) SortResult (mkSusp k2 (S.substitute DB.level0)) | (StypeLevel, Stype _) @@ -617,24 +617,24 @@ and check'' erased ctx e = if conv_p ctx t t' then () else log_tc_error - ~loc:(lexp_location e) + ~loc:(Lexp.location e) "Type mismatch for %s : %s != %s" - (lexp_string e) (lexp_string t) (lexp_string t') + (Lexp.to_string e) (Lexp.to_string t) (Lexp.to_string t') in let check_type erased ctx t = let s = check erased ctx t in (match lexp'_whnf s ctx with | Sort _ -> () | _ - -> let loc = lexp_location t in - log_tc_error ~loc "Not a proper type: %s" (lexp_string t)); + -> let loc = Lexp.location t in + log_tc_error ~loc "Not a proper type: %s" (Lexp.to_string t)); s in match lexp_lexp' e with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_integer | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _) | Symbol _ | Node (_, _, _)) - -> (log_tc_error ~loc:(lexp_location e) "Unsupported immediate value!"; + -> (log_tc_error ~loc:(Lexp.location e) "Unsupported immediate value!"; DB.type_int) | SortLevel SLz -> DB.type_level | SortLevel (SLsucc e) @@ -655,7 +655,7 @@ and check'' erased ctx e = mkSort (l, Stype (mkSortLevel (SLsucc e))) | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) - -> ((* error_tc ~loc:(lexp_location e) "Reached unreachable sort!"; + -> ((* error_tc ~loc:(Lexp.location e) "Reached unreachable sort!"; * Log.internal_error "Reached unreachable sort!"; *) DB.sort_omega) | Builtin (_, t) @@ -665,7 +665,7 @@ and check'' erased ctx e = | Var (((loc, name), idx) as v) -> if DB.set_mem idx erased then log_tc_error - ~loc:(sexp_location loc) + ~loc:(Sexp.location loc) {|Var `%s` can't be used here, because it's erasable|} (maybename name) ; lookup_type ctx v @@ -698,13 +698,13 @@ and check'' erased ctx e = match sort_compose ctx nctx loc ak k1 k2 with | SortResult k -> k | SortInvalid - -> log_tc_error ~loc:(sexp_location loc) "Invalid arrow: inner TypelLevel argument"; + -> log_tc_error ~loc:(Sexp.location loc) "Invalid arrow: inner TypelLevel argument"; mkSort (loc, StypeOmega) | SortK1NotType - -> log_tc_error ~loc:(lexp_location t1) "Not a proper type"; + -> log_tc_error ~loc:(Lexp.location t1) "Not a proper type"; mkSort (loc, StypeOmega) | SortK2NotType - -> log_tc_error ~loc:(lexp_location t2) "Not a proper type"; + -> log_tc_error ~loc:(Lexp.location t2) "Not a proper type"; mkSort (loc, StypeOmega)) | Lambda (ak, ((l,_) as v), t, e) -> (let _k = check_type DB.set_empty ctx t in @@ -721,12 +721,12 @@ and check'' erased ctx e = match lexp'_whnf ft ctx with | Arrow (_l, ak', _v, t1, t2) -> if ak != ak' - then log_tc_error ~loc:(lexp_location arg) "arg kind mismatch"; + then log_tc_error ~loc:(Lexp.location arg) "arg kind mismatch"; assert_type ctx arg at t1; mkSusp t2 (S.substitute arg) | _ -> log_tc_error - ~loc:(lexp_location arg) - "Calling a non functin (type = %s)!" (lexp_string ft); + ~loc:(Lexp.location arg) + "Calling a non functin (type = %s)!" (Lexp.to_string ft); ft) ft args | Inductive (l, _label, args, cases) @@ -752,18 +752,18 @@ and check'' erased ctx e = -> (if not(ak == P.Aerasable && impredicative_universe_poly) then log_tc_error - ~loc:(lexp_location t) + ~loc:(Lexp.location t) ~print_action:(fun _ -> ()) "Field of type %s not-allowed!" - (lexp_string t)); + (Lexp.to_string t)); level | _tt -> log_tc_error - ~loc:(lexp_location t) + ~loc:(Lexp.location t) ~print_action:(fun _ -> DB.print_lexp_ctx ictx; print_newline ()) "Field type %s is not a Type! (%s)" - (lexp_string t) (lexp_string lwhnf); + (Lexp.to_string t) (Lexp.to_string lwhnf); level), DB.lctx_extend ictx v Variable t, DB.set_sink 1 erased, @@ -803,20 +803,20 @@ and check'' erased ctx e = | [], [] -> s | _farg::fargs, (_ak, aarg)::aargs -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (log_tc_error ~loc:(sexp_location l) + | _,_ -> (log_tc_error ~loc:(Sexp.location l) "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes - : (arg_kind * vname * ltype) list) = + : (Pexp.ArgKind.t * vname * ltype) list) = match fieldtypes with - | [] -> log_tc_error ~loc:(sexp_location l) "Tuple has no field named: %s" label; + | [] -> log_tc_error ~loc:(Sexp.location l) "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:(sexp_location l) "Can't Proj an erasable field: %s" + else (log_tc_error ~loc:(Sexp.location l) "Can't Proj an erasable field: %s" label; Lexp.impossible) | (_, vdef, _)::fieldtypes @@ -828,10 +828,10 @@ and check'' erased ctx e = getfieldtype (S.cons fieldref s) fieldtypes in getfieldtype s fieldtypes | Inductive _, _ - -> Log.log_error ~loc:(sexp_location l) + -> Log.log_error ~loc:(Sexp.location l) "Proj on an inductive type that's not a tuple!"; etype - | _,_ -> Log.log_error ~loc:(sexp_location l) "Proj on a non-inductive type!" ; etype) + | _,_ -> Log.log_error ~loc:(Sexp.location l) "Proj on a non-inductive type!" ; etype) | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) @@ -845,7 +845,7 @@ and check'' erased ctx e = let ekind = get_type ctx etype in let elvl = match lexp'_whnf ekind ctx with | Sort (_, Stype l) -> l - | _ -> Log.log_error ~loc:(lexp_location ekind) + | _ -> Log.log_error ~loc:(Lexp.location ekind) "Target lexp's kind is not a sort"; DB.level0 in let it, aargs = call_split etype in (match lexp'_whnf it ctx, aargs with @@ -858,7 +858,7 @@ and check'' erased ctx e = * returns a valid type. *) -> mksubst (S.cons aarg s) fargs aargs | _ - -> log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; + -> log_tc_error ~loc:(Sexp.location l) "Wrong arg number to inductive type!"; s in let s = mksubst S.identity fargs aargs in let ctx_extend_with_eq ctx subst hlxp nerased = @@ -866,12 +866,12 @@ and check'' erased ctx e = let tltp = mkSusp etype subst in let tlvl = mkSusp elvl subst in let eqty = mkCall (l, DB.type_eq, - [(L.Aerasable, tlvl); (* Typelevel *) - (L.Aerasable, tltp); (* Inductive type *) - (L.Anormal, hlxp); (* Lexp of the branch head *) - (L.Anormal, tlxp)]) in (* Target lexp *) + [(Pexp.Aerasable, tlvl); (* Typelevel *) + (Pexp.Aerasable, tltp); (* Inductive type *) + (Pexp.Anormal, hlxp); (* Lexp of the branch head *) + (Pexp.Anormal, tlxp)]) in (* Target lexp *) (* The eq proof is erasable. *) - let nerased = dbset_push L.Aerasable nerased in + let nerased = dbset_push Pexp.Aerasable nerased in let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in (nerased, nctx) in SMap.iter @@ -889,10 +889,10 @@ and check'' erased ctx e = (mkCall (l, mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) vdefs fieldtypes | _ - -> log_tc_error ~loc:(sexp_location l) "Wrong number of args to constructor!"; + -> log_tc_error ~loc:(Sexp.location l) "Wrong number of args to constructor!"; (erased, ctx, hlxp) in let hctor = - mkCall (l, mkCons (it, (sexp_location l, name)), + mkCall (l, mkCons (it, (Sexp.location l, name)), List.map (fun (_, a) -> (P.Aerasable, a)) aargs) in let (nerased, nctx, hlxp) = mkctx erased ctx s hctor vdefs fieldtypes in @@ -906,7 +906,7 @@ and check'' erased ctx e = (match default with | Some (v, d) -> if diff <= 0 - then log_tc_warning ~loc:(sexp_location l) "Redundant default clause"; + then log_tc_warning ~loc:(Sexp.location l) "Redundant default clause"; let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in let nerased = DB.set_sink 1 erased in let subst = S.shift 1 in @@ -919,8 +919,8 @@ and check'' erased ctx e = -> if diff > 0 then log_tc_error - ~loc:(sexp_location l) "Non-exhaustive match: %d cases missing" diff) - | _,_ -> log_tc_error ~loc:(sexp_location l) "Case on a non-inductive type!"); + ~loc:(Sexp.location l) "Non-exhaustive match: %d cases missing" diff) + | _,_ -> log_tc_error ~loc:(Sexp.location l) "Case on a non-inductive type!"); ret | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with @@ -949,11 +949,11 @@ and check'' erased ctx e = buildtype fargs with | Not_found - -> log_tc_error ~loc:(sexp_location l) {|Constructor "%s" does not exist|} name; + -> log_tc_error ~loc:(Sexp.location l) {|Constructor "%s" does not exist|} name; DB.type_int) | _ -> log_tc_error - ~loc:(lexp_location e) - "Cons of a non-inductive type: %s" (lexp_string t); + ~loc:(Lexp.location e) + "Cons of a non-inductive type: %s" (Lexp.to_string t); DB.type_int) | Metavar (idx, s, _) -> (match metavar_lookup idx with @@ -1118,21 +1118,21 @@ and get_type ctx e = | [], [] -> s | _farg::fargs, (_ak, aarg)::aargs -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (log_tc_error ~loc:(sexp_location l) + | _,_ -> (log_tc_error ~loc:(Sexp.location l) "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes - : (arg_kind * vname * ltype) list) = + : (Pexp.ArgKind.t * vname * ltype) list) = match fieldtypes with - | [] -> log_tc_error ~loc:(sexp_location l) "Tuple has no field named: %s" + | [] -> log_tc_error ~loc:(Sexp.location l) "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:(sexp_location l) + else (log_tc_error ~loc:(Sexp.location l) "Can't Proj an erasable field: %s" label; Lexp.impossible) | (_, vdef, _)::fieldtypes @@ -1144,10 +1144,10 @@ and get_type ctx e = getfieldtype (S.cons fieldref s) fieldtypes in getfieldtype s fieldtypes | Inductive _, _ - -> Log.log_error ~loc:(sexp_location l) + -> Log.log_error ~loc:(Sexp.location l) "Proj on an inductive type that's not a tuple!"; etype - | _,_ -> Log.log_error ~loc:(sexp_location l) "Proj on a non-inductive type!" ; + | _,_ -> Log.log_error ~loc:(Sexp.location l) "Proj on a non-inductive type!" ; etype) | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) @@ -1264,7 +1264,7 @@ let arity_of_cons : int = let count_unless_erasable i = function - | (Aerasable, _, _) -> i + | (Pexp.Aerasable, _, _) -> i | _ -> i + 1 in @@ -1275,10 +1275,10 @@ let arity_of_cons | None -> error ~location "invalid constructor: %s" name) | _ -> error - ~location:(lexp_location ty) + ~location:(Lexp.location ty) ({|can't deduce arity of constructor "%s", |} ^^ {|because it is not an inductive type: %s|}) - name (lexp_string ty) + name (Lexp.to_string ty) let pos_of_label lctx label e : int = @@ -1295,7 +1295,7 @@ let pos_of_label lctx label e : int = (match SMap.bindings constructors with | [(_,l)] -> let rec find_index label - (l : (arg_kind * vname * ltype) list) + (l : (Pexp.ArgKind.t * vname * ltype) list) (c: int) : int = match l with | [] @@ -1315,7 +1315,7 @@ let pos_of_label lctx label e : int = 0 | _,_ -> let (loc,_) = label in Log.log_error ~loc:loc "Proj on a non-inductive type: %s" - (Lexp.lexp_string it); + (Lexp.to_string it); 0 @@ -1326,7 +1326,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Var (v) -> E.Var (v) | L.Proj (l, exp, label) -> let t = get_type lctx exp in - E.Proj (sexp_location l, erase_type lctx exp, pos_of_label lctx label t) + E.Proj (Sexp.location l, erase_type lctx exp, pos_of_label lctx label t) | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s) | L.Lambda (P.Aerasable, _, _, body) @@ -1338,7 +1338,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Let (l, decls, body) -> let lctx', edecls = clean_decls lctx decls in - E.Let (sexp_location l, edecls, erase_type lctx' body) + E.Let (Sexp.location l, edecls, erase_type lctx' body) | L.Call (_, fct, args) -> E.Call (erase_type lctx fct, List.filter_map (clean_arg lctx) args) @@ -1346,7 +1346,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Case (location, target, _, branches, default) -> let etarget = erase_type lctx target in let ebranches = clean_branch_map lctx branches in - E.Case (sexp_location location, etarget, ebranches, clean_default lctx default) + E.Case (Sexp.location location, etarget, ebranches, clean_default lctx default) | L.Susp (l, s) -> erase_type lctx (L.push_susp l s) @@ -1395,7 +1395,7 @@ and clean_branch_map lctx cases = in let eargs, subst, lctx' = clean_arg_list args [] S.identity lctx in let subst = S.cons erasure_dummy subst in (* Substitute the equality. *) - (sexp_location l, eargs, erase_type lctx' (L.push_susp expr subst)) + (Sexp.location l, eargs, erase_type lctx' (L.push_susp expr subst)) in SMap.map clean_branch cases @@ -1408,9 +1408,9 @@ let erase_type lctx lxp = Log.log_fatal ~print_action:(fun () -> IMap.iter (fun i (_, t, _, (l, n)) -> - print_endline ("\t" ^ (Source.Location.to_string (sexp_location l)) + print_endline ("\t" ^ (Source.Location.to_string (Sexp.location l)) ^ " ?" ^ (Option.value ~default:"" n) - ^ "[" ^ (string_of_int i) ^ "] : " ^ (lexp_string t)) + ^ "[" ^ (string_of_int i) ^ "] : " ^ (Lexp.to_string t)) ) mvs) ("Metavariables in erase_type :"); erase_type lctx lxp @@ -1442,8 +1442,8 @@ let ctx2tup ctx nctx = match blocs with | [] -> let cons_name = "cons" in - let cons_label = (sexp_location loc, cons_name) in - let type_label = (sexp_location loc, "record") in + let cons_label = (Sexp.location loc, cons_name) in + let type_label = (Sexp.location loc, "record") in let offset = List.length types in let types = List.rev types in (*Log.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*) ===================================== src/pexp.ml ===================================== @@ -26,10 +26,20 @@ let pexp_error loc = Log.log_error ~section:"PEXP" ~loc (*************** The Pexp Parser *********************) +type arg_kind = + | Anormal + | Aimplicit + | Aerasable (** eraseable ⇒ implicit. *) + module ArgKind = struct - type arg_kind = Anormal | Aimplicit | Aerasable (* eraseable ⇒ implicit. *) + type t = arg_kind + + let to_arrow : t -> string = function + | Anormal -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>" + + let to_colon : t -> string = function + | Anormal -> ":" | Aimplicit -> "::" | Aerasable -> ":::" end -include ArgKind (* This is Dangerously misleading since pvar is NOT pexp but Pvar is *) type pvar = symbol @@ -41,7 +51,7 @@ type ppat = | Ppatcons of Source.Location.t * sexp * (symbol option * vname) list let pexp_pat_location : ppat -> Source.Location.t = function - | Ppatsym (l, _) -> sexp_location l + | Ppatsym (l, _) -> Sexp.location l | Ppatcons (l, _, _) -> l let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = @@ -54,33 +64,32 @@ let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = | Anormal -> ":") in let ty = match t with Some e -> e | None -> Symbol (l, "_") in - let location = Source.Location.extend l (sexp_location ty) in + let location = Source.Location.extend l (Sexp.location ty) in Node (location, head, [Symbol s; ty]) let pexp_p_pat_arg (s : sexp) = match s with | Symbol (_l , n) -> (None, (s, match n with "_" -> None | _ -> Some n)) | Node (_, Symbol (_, "_:=_"), [Symbol f; Symbol (_l,n)]) -> (Some f, (s, Some n)) - | _ -> let loc = sexp_location s in - pexp_error loc "Unknown pattern arg"; - (None, (s, None)) + | _ + -> let loc = Sexp.location s in + pexp_error loc "Unknown pattern arg"; + (None, (s, None)) -let pexp_u_pat_arg (okn, (l, oname) : symbol option * vname) : sexp = - let oname_text = match oname with None -> "_" | Some n -> n in - let pname = Sexp.symbol ~location:(sexp_location l) oname_text in +let pexp_u_pat_arg ((okn, (l, oname)) : symbol option * vname) : sexp = + let pname = Symbol (Sexp.location l, match oname with None -> "_" | Some n -> n) in match okn with | None -> pname | Some ((l, _) as n) -> Node (l, Symbol (l, "_:=_"), [Symbol n; pname]) let pexp_p_pat (s : sexp) : ppat = match s with | Symbol (_l, n) -> Ppatsym (s, match n with "_" -> None | _ -> Some n) - | Node (location, c, args) - -> Ppatcons (location, c, List.map pexp_p_pat_arg args) + | Node (l, c, args) -> Ppatcons (l, c, List.map pexp_p_pat_arg args) | _ - -> pexp_error (sexp_location s) "Unknown pattern"; - Ppatsym (s, None) + -> let l = Sexp.location s in + pexp_error l "Unknown pattern"; Ppatsym (s, None) let pexp_u_pat (p : ppat) : sexp = match p with - | Ppatsym (l, None) -> Symbol (sexp_location l, "_") - | Ppatsym (l, Some n) -> Symbol (sexp_location l, n) - | Ppatcons (location, c, args) -> Node (location, c, List.map pexp_u_pat_arg args) + | Ppatsym (l, None) -> Symbol (Sexp.location l, "_") + | Ppatsym (l, Some n) -> Symbol (Sexp.location l, n) + | Ppatcons (l, c, args) -> Node (l, c, List.map pexp_u_pat_arg args) ===================================== src/prelexer.ml ===================================== @@ -1,6 +1,6 @@ (* prelexer.ml --- First half of lexical analysis of Typer. -Copyright (C) 2011-2021 Free Software Foundation, Inc. +Copyright (C) 2011-2023 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> Keywords: languages, lisp, dependent types. @@ -32,16 +32,47 @@ type pretoken = module Pretoken = struct type t = pretoken - (* Equality up to location, i.e. the location is not considered. *) - let rec equal (l : t) (r : t) = + (** Equality up to location, i.e. the location is not considered. *) + let rec equal (l : t) (r : t) : bool = match l, r with | Pretoken (_, l_name), Pretoken (_, r_name) -> String.equal l_name r_name | Prestring (_, l_text), Prestring (_, r_text) -> String.equal l_text r_text | Preblock (_, l_inner), Preblock (_, r_inner) - -> Listx.equal equal l_inner r_inner + -> List.equal equal l_inner r_inner | _ -> false + + (** Equality, considering location information. *) + let rec same (l : t) (r : t) : bool = + match l, r with + | Pretoken (l_location, l_name), Pretoken (r_location, r_name) + -> Source.Location.same l_location r_location + && String.equal l_name r_name + | Prestring (l_location, l_text), Prestring (r_location, r_text) + -> Source.Location.same l_location r_location + && String.equal l_text r_text + | Preblock (l_location, l_inner), Preblock (r_location, r_inner) + -> Source.Location.same l_location r_location + && List.equal same l_inner r_inner + | _ -> false + + let location : t -> Source.Location.t = function + | Preblock (location, _) | Pretoken (location, _) | Prestring (location, _) + -> location + + let rec pp_print (f : Format.formatter) (pretoken : t) : unit = + Format.pp_open_stag f (Source.Located (location pretoken)); + begin match pretoken with + | Preblock (_, pretokens) + -> Format.fprintf f "@[<hov 1>{%a}@]" pp_print_list pretokens + | Pretoken (_, text) -> Format.pp_print_string f text + | Prestring (_, text) -> Format.fprintf f {|"%s"|} text + end; + Format.pp_close_stag f () + + and pp_print_list (f : Format.formatter) (pretokens : t list) : unit = + Format.pp_print_list ~pp_sep:Format.pp_print_space pp_print f pretokens end (*************** The Pre-Lexer phase *********************) @@ -185,49 +216,3 @@ let prelex (source : #Source.t) : pretoken list = in pretok () in loop [] [] - -let pretoken_name : pretoken -> string = function - | Pretoken _ -> "Pretoken" - | Prestring _ -> "Prestring" - | Preblock _ -> "Preblock" - -let rec pretoken_string' (output : string -> unit) : pretoken -> unit = function - | Preblock (_, []) -> - output "{}" - | Preblock (_, head :: tail) -> - output "{"; - pretoken_string' output head; - List.iter (fun pt -> output " "; pretoken_string' output pt) tail; - output "}" - | Pretoken (_, text) -> - output text - | Prestring (_, text) -> - output {|"|}; - output text; - output {|"|} - -let pretoken_string (pretoken : pretoken) : string = - let buffer = Buffer.create 32 in - pretoken_string' (Buffer.add_string buffer) pretoken; - Buffer.contents buffer - -let pretokens_string (pretokens : pretoken list) : string = - let buffer = Buffer.create 32 in - List.iter (pretoken_string' (Buffer.add_string buffer)) pretokens; - Buffer.contents buffer - -let pretokens_print : pretoken list -> unit = - List.iter (pretoken_string' print_string) - -(* Prelexer comparison, ignoring source-line-number info, used for tests. *) -let rec pretokens_equal p1 p2 = match p1, p2 with - | Pretoken (_, s1), Pretoken (_, s2) -> s1 = s2 - | Prestring (_, s1), Prestring (_, s2) -> s1 = s2 - | Preblock (_, ps1), Preblock (_, ps2) -> - pretokens_eq_list ps1 ps2 - | _ -> false -and pretokens_eq_list ps1 ps2 = match ps1, ps2 with - | [], [] -> true - | (p1 :: ps1), (p2 :: ps2) -> - pretokens_equal p1 p2 && pretokens_eq_list ps1 ps2 - | _ -> false ===================================== src/sexp.ml ===================================== @@ -1,6 +1,6 @@ (* sexp.ml --- The Lisp-style Sexp abstract syntax tree. -Copyright (C) 2011-2021 Free Software Foundation, Inc. +Copyright (C) 2011-2023 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> Keywords: languages, lisp, dependent types. @@ -26,8 +26,6 @@ open Prelexer let sexp_error ?print_action loc fmt = Log.log_error ~section:"SEXP" ?print_action ~loc fmt -type integer = Z.t - module Sym = struct type t = Source.Location.t * string @@ -53,6 +51,9 @@ module Sym = struct let same (l : t) (r : t) : bool = Source.Location.same (location l) (location r) && name l = name r + + let pp_print (f : Format.formatter) (_, name : t) : unit = + Format.pp_print_string f name end type symbol = Sym.t @@ -61,7 +62,7 @@ type t = | Block of Source.Location.t * pretoken list | Symbol of Sym.t | String of Source.Location.t * string - | Integer of Source.Location.t * integer + | Integer of Source.Location.t * Z.t | Float of Source.Location.t * float | Node of Source.Location.t * t * t list type sexp = t @@ -75,7 +76,6 @@ let location : sexp -> location = function | Integer (l, _) -> l | Float (l, _) -> l | Node (l, _, _) -> l -let sexp_location = location let symbol ~(location : Source.Location.t) (name : string) : t = Symbol (Sym.intern ~location name) @@ -98,6 +98,15 @@ let dummy_sinfo = epsilon dummy_location type vname = sinfo * string option type vref = vname * db_index +let string_of_vname ?(default : string = "<anon>") : vname -> string = function + | (_, None) -> default + | (_, Some (name)) -> name + +let pp_print_vname + ?(default : string option) (f : Format.formatter) (name : vname) + : unit = + Format.pp_print_string f (string_of_vname ?default name) + (********************** Sexp tests **********************) let pred_symbol s pred = @@ -107,33 +116,34 @@ let pred_symbol s pred = (*************** The Sexp Printer *********************) -(* Converts a sexp to a string, optionally printing locations as a list preceded - by a Racket-style reader comment (#;). *) -let rec sexp_string ?(print_locations = false) sexp = - (if print_locations - then - let open Source.Location in - let {container; start; end'} = sexp_location sexp - in - Printf.sprintf - "#;(\"%s\" %d %d %d %d %d %d) " - (Source.Container.name container) - start.offset start.line start.column - end'.offset end'.line end'.column - else "") - ^ match sexp with - | Block(_, pts) -> "{" ^ (pretokens_string pts) ^ " }" - | Symbol(_, "") -> "()" (* Epsilon *) - | Symbol(_, name) -> name - | String(_, str) -> "\"" ^ str ^ "\"" - | Integer(_, n) -> Z.to_string n - | Float(_, x) -> string_of_float x - | Node(_, f, args) -> - let str = "(" ^ (sexp_string ~print_locations f) in - (List.fold_left (fun str sxp -> - str ^ " " ^ (sexp_string ~print_locations sxp)) str args) ^ ")" - -let sexp_print sexp = print_string (sexp_string sexp) +let rec pp_print (f : Format.formatter) (sexp : sexp) : unit = + Format.pp_open_stag f (Source.Located (location sexp)); + begin match sexp with + | Block (_, pretokens) + -> Format.fprintf f "@[<hov 1>{%a}@]" Pretoken.pp_print_list pretokens + | Symbol (_, "") + -> Format.pp_print_string f "ε" + | Symbol (_, name) + -> Format.pp_print_string f name + | String (_, value) + -> Format.fprintf f {|"%s"|} (String.escaped value) + | Integer (_, value) + -> Z.pp_print f value + | Float (_, value) + -> Format.pp_print_float f value + | Node (_, head, tail) + -> Format.fprintf f "@[<hov 1>(%a)@]" pp_print_list (head :: tail) + end; + Format.pp_close_stag f () + +and pp_print_list (f : Format.formatter) (sexps : sexp list) : unit = + Format.pp_print_list ~pp_sep:Format.pp_print_space pp_print f sexps + +let to_string (sexp : sexp) : string = + Format.asprintf "%a" pp_print sexp + +let print (sexp : sexp) : unit = + Format.printf "%a" pp_print sexp let sexp_name s = match s with @@ -305,13 +315,13 @@ let sexp_parse_all_to_list grm tokens limit : sexp list = (** Sexp comparison, ignoring source-line-number info, used for tests. *) let rec sexp_equal s1 s2 = match s1, s2 with - | Block (_, ps1), Block (_, ps2) -> pretokens_eq_list ps1 ps2 + | Block (_, ps1), Block (_, ps2) -> List.equal Pretoken.equal ps1 ps2 | Symbol (_, s1), Symbol (_, s2) -> s1 = s2 | String (_, s1), String (_, s2) -> s1 = s2 | Integer (_, n1), Integer (_, n2) -> n1 = n2 | Float (_, n1), Float (_, n2) -> n1 = n2 | Node (_, s1, ss1), Node (_, s2, ss2) - -> sexp_equal s1 s2 && Listx.equal sexp_equal ss1 ss2 + -> sexp_equal s1 s2 && List.equal sexp_equal ss1 ss2 | _ -> false (** Sexp comparison, *with* source-line-number info, used for tests. *) @@ -319,7 +329,7 @@ let rec same l r = match l, r with | Block (l_location, l_pretokens), Block (r_location, r_pretokens) -> Source.Location.same l_location r_location - && Listx.equal pretokens_equal l_pretokens r_pretokens + && List.equal Pretoken.same l_pretokens r_pretokens | Symbol (l_sym), Symbol (r_sym) -> Sym.same l_sym r_sym | String (l_location, l_value), String (r_location, r_value) @@ -334,5 +344,5 @@ let rec same l r = | Node (l_location, l_head, l_tail), Node (r_location, r_head, r_tail) -> Source.Location.same l_location r_location && same l_head r_head - && Listx.equal same l_tail r_tail + && List.equal same l_tail r_tail | _, _ -> false ===================================== src/source.ml ===================================== @@ -179,6 +179,30 @@ module Location = struct {container = l.container; start; end'} end +type Format.stag += Located of Location.t + +let pp_enable_print_locations (f : Format.formatter) : unit = + let fns = Format.pp_get_formatter_stag_functions f () in + let fns' = + { + fns with + print_open_stag = + begin function + | Located (location) + -> Format.fprintf f "@[<hov 0>%a@ " Location.pp_print location + | stag -> fns.print_open_stag stag + end; + print_close_stag = + begin function + | Located _ + -> Format.pp_close_box f () + | stag -> fns.print_close_stag stag + end; + } + in + Format.pp_set_formatter_stag_functions f fns'; + Format.pp_set_tags f true + (** A source object is text paired with a cursor. The text can be lazily loaded as it is accessed byte by byte, but it must be retained for future reference by error messages. *) ===================================== src/unification.ml ===================================== @@ -331,8 +331,8 @@ and unify_metavar (matching : scope_level option) | exception Inverse_subst.Not_invertible -> log_info "Unification of metavar failed:\n ?[%s]\nAgainst:\n %s\n" - (subst_string s) - (lexp_string lxp); + (Format.asprintf "%a" Lexp.pp_print_subst s) + (Lexp.to_string lxp); [(CKresidual, ctx, lxp1, lxp2)] | lxp' when occurs_in idx lxp' -> [(CKimpossible, ctx, lxp1, lxp2)] | lxp' @@ -344,9 +344,9 @@ and unify_metavar (matching : scope_level option) | _ -> log_info "Unificaton of metavar type failed:\n %s != %s\nfor %s\n" - (lexp_string t) - (lxp |> OL.get_type ctx |> lexp_string) - (lexp_string lxp); + (Lexp.to_string t) + (lxp |> OL.get_type ctx |> Lexp.to_string) + (Lexp.to_string lxp); [(CKresidual, ctx, lxp1, lxp2)] in (* FIXME Here, we unify lxp1 with lxp2 again, because that the metavariables occuring in the associated term might ===================================== src/util.ml ===================================== @@ -23,8 +23,6 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) module SMap = Map.Make(String) module IMap = Map.Make(Int) -type charpos = int -type bytepos = int type location = Source.Location.t let dummy_location = Source.Location.dummy @@ -77,27 +75,6 @@ let str_split str sep = let utf8_head_p (c : char) : bool = Char.code c < 128 || Char.code c >= 192 -(* Display size of `str`, assuming the byte-sequence is UTF-8. - * Very naive: doesn't pay attention to LF, TABs, double-width chars, ... *) -let string_width (s : string) : int = - let rec width i w = - if i < 0 then w - else width (i - 1) - (if utf8_head_p (String.get s i) - then w + 1 - else w) in - width (String.length s - 1) 0 - -let padding_right (str: string ) (dim: int ) (char_: char) : string = - let diff = (dim - string_width str) - in let rpad = max diff 0 - in str ^ (String.make rpad char_) - -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 - (* It seemed good to use the prime number 31. * FIXME: Pick another one ? *) let combine_hash e1 e2 = (e1 * 31) lxor e2 ===================================== tests/instargs_test.ml ===================================== @@ -208,7 +208,7 @@ let _ = let limit = 20 in Instargs.recursion_limit := Some limit; let lxp = snat_metavar limit snats_ectx in - expect_throw L.lexp_string + expect_throw Lexp.to_string (fun _ -> E.resolve_instances lxp; Log.stop_on_error (); lxp)) let _ = run_all () ===================================== tests/lexer_test.ml ===================================== @@ -27,22 +27,25 @@ open Sexp let test_lex name pretokens expected = let lex () = let actual = Lexer.lex Grammar.default_stt pretokens in - if Listx.equal Sexp.same actual expected + if List.equal Sexp.same actual expected then success else - ((* Only print locations if the Sexp are otherwise identical so its easier - to spot the problem. *) - let print_locations = - Listx.equal Sexp.sexp_equal actual expected - in - let print_token token = - Printf.printf "%s\n" (sexp_string ~print_locations token) - in - Printf.printf "%sExpected:%s\n" Fmt.red Fmt.reset; - List.iter print_token expected; - Printf.printf "%sActual:%s\n" Fmt.red Fmt.reset; - List.iter print_token actual; - failure) + begin + (* Only print locations if the Sexp are otherwise identical so its + easier to spot the problem. *) + let open Format in + let f = formatter_of_out_channel stderr in + if List.equal Sexp.sexp_equal actual expected then + Source.pp_enable_print_locations f; + fprintf + f + "@{<red>Expected:@}@.%a@.@{<red>Actual:@}@.%a@." + Sexp.pp_print_list + expected + Sexp.pp_print_list + actual; + failure + end in add_test "LEXER" name lex ===================================== tests/positivity_test.ml ===================================== @@ -21,24 +21,22 @@ open Typerlib open Utest_lib -open Lexp open Positivity -(*open Util*) -exception WrongPolarity of vname +exception WrongPolarity of Sexp.vname type polarity = | Positive | Negative -let print_lexp lexp = ut_string 3 (Lexp.lexp_string lexp ^ "\n") +let print_lexp lexp = ut_string 3 (Lexp.to_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 lexp_decl_str (source : string) : (Sexp.vname * Lexp.lexp) list = let (decls, _) = Elab.lexp_decl_str source Elab.default_ectx in assert (List.length decls > 0); let decls = List.flatten decls in ===================================== tests/unify_test.ml ===================================== @@ -71,8 +71,8 @@ let add_unif_test name ?matching ?(ectx=ectx) lxp_a lxp_b expected = else ( ut_string2 (red ^ "EXPECTED: " ^ reset ^ (string_of_result expected) ^ "\n"); ut_string2 (red ^ "GOT: " ^ reset ^ (string_of_result r ) ^ "\n"); - ut_string2 ("During the unification of:\n\t" ^ (lexp_string lxp_a) - ^ "\nand\n\t" ^ (lexp_string lxp_b) ^ "\n"); + ut_string2 ("During the unification of:\n\t" ^ (Lexp.to_string lxp_a) + ^ "\nand\n\t" ^ (Lexp.to_string lxp_b) ^ "\n"); failure )) ===================================== tests/utest_lib.ml ===================================== @@ -135,21 +135,21 @@ let expect_equal_float = _expect_equal_t Float.equal string_of_float let expect_equal_str = _expect_equal_t String.equal (fun g -> g) let expect_equal_values = _expect_equal_t Env.value_eq_list print_value_list -let expect_equal_lexp = _expect_equal_t Lexp.eq Lexp.lexp_string -let expect_conv_lexp ctx = _expect_equal_t (Opslexp.conv_p ctx) Lexp.lexp_string +let expect_equal_lexp = _expect_equal_t Lexp.eq Lexp.to_string +let expect_conv_lexp ctx = _expect_equal_t (Opslexp.conv_p ctx) Lexp.to_string let expect_equal_sexps ~expected ~actual = let print_sexp_ok s = - Printf.printf (green_f ^^ "%s" ^^ reset_f ^^ "\n") (Sexp.sexp_string s) + Printf.printf (green_f ^^ "%s" ^^ reset_f ^^ "\n") (Sexp.to_string s) in let print_sexp_err expected actual = Printf.printf ("Expected:\n" ^^ red_f ^^ "%s\n" ^^ reset_f) - (Sexp.sexp_string expected); + (Sexp.to_string expected); Printf.printf ("Actual:\n" ^^ red_f ^^ "%s\n" ^^ reset_f) - (Sexp.sexp_string actual) + (Sexp.to_string actual) in let rec loop failed fine expected actual = @@ -164,13 +164,13 @@ let expect_equal_sexps ~expected ~actual = | _ :: _, [] -> List.iter print_sexp_ok fine; Printf.printf ("Missing sexps:\n" ^^ red_f); - List.iter (fun s -> s |> Sexp.sexp_string |> Printf.printf "%s\n") expected; + List.iter (fun s -> s |> Sexp.to_string |> Printf.printf "%s\n") expected; Printf.printf reset_f; true | [], _ :: _ -> List.iter print_sexp_ok fine; Printf.printf ("Unexpected sexps:\n" ^^ red_f); - List.iter (fun s -> s |> Sexp.sexp_string |> Printf.printf "%s\n") actual; + List.iter (fun s -> s |> Sexp.to_string |> Printf.printf "%s\n") actual; Printf.printf reset_f; true | [], [] -> @@ -191,7 +191,7 @@ let expect_equal_lexps = | _ -> false in let string_of_lexp_list lexps = - List.fold_left (fun s lexp -> s ^ "\n" ^ Lexp.lexp_string lexp) "" lexps + List.fold_left (fun s lexp -> s ^ "\n" ^ Lexp.to_string lexp) "" lexps in _expect_equal_t lexp_list_eq string_of_lexp_list @@ -218,17 +218,7 @@ let expect_equal_decls = | _ -> false in let string_of_decl_list ds = - let buffer = Buffer.create 1024 in - let string_of_mutual_decl_list ds = - let source = Lexp.lexp_str_decls Lexp.pretty_ppctx ds in - let add_decl d = - Buffer.add_string buffer d; - Buffer.add_char buffer '\n' - in - List.iter add_decl source - in - List.iter string_of_mutual_decl_list ds; - Buffer.contents buffer + Format.asprintf "%a" Lexp.pp_print_decls ds in _expect_equal_t decl_list_eq string_of_decl_list ===================================== typer.ml ===================================== @@ -1,4 +1,4 @@ -(* Copyright (C) 2021 Free Software Foundation, Inc. +(* Copyright (C) 2021-2023 Free Software Foundation, Inc. * * Author: Simon Génier <simon.genier(a)umontreal.ca> * Keywords: languages, lisp, dependent types. @@ -47,7 +47,7 @@ let arg_defs = "Trace macro expansion"); ] -let parse_args argv usage = +let parse_args ?(arg_defs = arg_defs) argv usage = try Arg.parse_argv argv arg_defs add_input_file usage with | Arg.Help (message) -> print_string message; @@ -103,6 +103,91 @@ let run_main argv = in Log.print_log () +let dump_pretokens_main argv = + let usage = Sys.executable_name ^ " dump-pretokens <file> …" in + let arg_defs = [] in + parse_args ~arg_defs argv usage; + + let dump_pretokens_of_file path = + let source = Source.of_path path in + let pretokens = Prelexer.prelex source in + let f = Fmt.formatter_of_out_channel stdout in + Source.pp_enable_print_locations f; + Format.fprintf f "@[<v>%a@]@." Prelexer.Pretoken.pp_print_list pretokens + in + List.iter dump_pretokens_of_file (list_input_files ()) + +let dump_tokens_main argv = + let usage = Sys.executable_name ^ " dump-tokens <file> …" in + let arg_defs = [] in + parse_args ~arg_defs argv usage; + + let dump_tokens_of_file path = + let source = Source.of_path path in + let pretokens = Prelexer.prelex source in + let tokens = Lexer.lex Grammar.default_stt pretokens in + let f = Fmt.formatter_of_out_channel stdout in + Source.pp_enable_print_locations f; + Format.fprintf f "@[<v>%a@]@." Sexp.pp_print_list tokens + in + List.iter dump_tokens_of_file (list_input_files ()) + +let print_indices = ref false +let dump_lexps_arg_defs = + [ + ("-Vindices", + Arg.Set print_indices, + "Print Debruijn indices in addition to variable names."); + ] + +let dump_lexps_main argv = + let usage = Sys.executable_name ^ " dump-lexps <file> …" in + parse_args ~arg_defs:dump_lexps_arg_defs argv usage; + + let dump_lexps_of_file ectx path = + let source = Source.of_path path in + let pretokens = Prelexer.prelex source in + let tokens = Lexer.lex Grammar.default_stt pretokens in + let ldecls, ectx' = Elab.lexp_p_decls [] tokens ectx in + let f = Fmt.formatter_of_out_channel stdout in + if !print_indices then + Lexp.pp_enable_print_indices f; + Format.fprintf f "%a@." Lexp.pp_print_decls ldecls; + ectx' + in + let _ = + List.fold_left + dump_lexps_of_file + Elab.default_ectx + (list_input_files ()) + in + () + +let dump_elexps_main argv = + let usage = Sys.executable_name ^ " dump-elexps <file> …" in + parse_args ~arg_defs:dump_lexps_arg_defs argv usage; + + let dump_elexps_of_file ectx path = + let source = Source.of_path path in + let pretokens = Prelexer.prelex source in + let tokens = Lexer.lex Grammar.default_stt pretokens in + let ldecls, ectx' = Elab.lexp_p_decls [] tokens ectx in + let lctx = Debruijn.ectx_to_lctx ectx' in + let _, eldecls = List.fold_left_map Opslexp.clean_decls lctx ldecls in + let f = Fmt.formatter_of_out_channel stdout in + if !print_indices then + Lexp.pp_enable_print_indices f; + Format.fprintf f "%a@." Elexp.pp_print_decls eldecls; + ectx' + in + let _ = + List.fold_left + dump_elexps_of_file + Elab.default_ectx + (list_input_files ()) + in + () + let main () = let command, argv = if Array.length Sys.argv <= 1 @@ -125,6 +210,10 @@ let main () = | "compile" -> compile_main argv | "repl" -> repl_main argv | "run" -> run_main argv + | "dump-pretokens" -> dump_pretokens_main argv + | "dump-tokens" -> dump_tokens_main argv + | "dump-lexps" -> dump_lexps_main argv + | "dump-elexps" -> dump_elexps_main argv | _ -> eprintf {|unknown command "%s"|} command; exit 1) View it on GitLab: https://gitlab.com/monnier/typer/-/compare/22282068fd8f352abaeaccf116efa190… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/22282068fd8f352abaeaccf116efa190… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][simon--pp-print] 6 commits: Fix an inf-loop during elaboration
by Simon Génier (＠ilovemonoids) 22 Mar '23

22 Mar '23

Simon Génier pushed to branch simon--pp-print at Stefan / Typer Commits: 4421b8e7 by Stefan Monnier at 2023-03-21T23:25:52-04:00 Fix an inf-loop during elaboration When `typer-identifier` is redefined as something else than a special form or a macro, we got into an inf-loop when elaborating X because we would rewrite to (typer_identifier X), which would then be taken as a function call, which recursively elaborates its arg X, ... * src/elab.ml (sform_immediate, sform_identifier): Move before `elaborate`. (elab_via): New function. (elaborate): Use it. - - - - - 22282068 by Simon Génier at 2023-03-22T18:03:27-04:00 Merge branch 'simon--source-container' - - - - - e13d2142 by Simon Génier at 2023-03-22T18:05:48-04:00 Use format to print pretokens. - - - - - e350b2d7 by Simon Génier at 2023-03-22T18:10:14-04:00 Use Format to print sexps. - - - - - 08503fe0 by Simon Génier at 2023-03-22T18:10:18-04:00 Use Format to print lexps. - - - - - 9f89fdce by Simon Génier at 2023-03-22T18:10:18-04:00 Use Format to print elexps. - - - - - 27 changed files: - − .idea/workspace.xml - debug_util.ml - src/debruijn.ml - − src/debug.ml - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/fmt.ml - src/gambit.ml - src/instargs.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml - src/listx.ml → src/list.ml - src/opslexp.ml - src/pexp.ml - src/prelexer.ml - src/sexp.ml - src/source.ml - src/unification.ml - src/util.ml - tests/instargs_test.ml - tests/lexer_test.ml - tests/positivity_test.ml - tests/unify_test.ml - tests/utest_lib.ml The diff was not included because it is too large. View it on GitLab: https://gitlab.com/monnier/typer/-/compare/1778c81f7946d416fa5e467e8b0f5a96… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/1778c81f7946d416fa5e467e8b0f5a96… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch simon--source-container
by Simon Génier (＠ilovemonoids) 22 Mar '23

22 Mar '23

Simon Génier deleted branch simon--source-container at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][main] 2 commits: Save contents of a source file so locations can refer to it.
by Simon Génier (＠ilovemonoids) 22 Mar '23

22 Mar '23

Simon Génier pushed to branch main at Stefan / Typer Commits: 14166a24 by Simon Génier at 2023-02-21T12:46:55-05:00 Save contents of a source file so locations can refer to it. - - - - - 22282068 by Simon Génier at 2023-03-22T18:03:27-04:00 Merge branch 'simon--source-container' - - - - - 11 changed files: - debug_util.ml - src/REPL.ml - src/debug.ml - src/elab.ml - src/eval.ml - src/lexer.ml - src/sexp.ml - src/source.ml - src/string.ml - tests/lexer_test.ml - tests/sexp_test.ml Changes: ===================================== debug_util.ml ===================================== @@ -174,7 +174,7 @@ let format_source () = print_string (make_title " ERRORS "); let filename = List.hd (!arg_files) in - let source = new Source.source_file filename in + let source = Source.of_path filename in let pretoks = prelex source in let toks = lex default_stt pretoks in let ctx = Elab.default_ectx in @@ -218,7 +218,7 @@ let main () = (* get pretokens*) print_string yellow; - let source = new Source.source_file filename in + let source = Source.of_path filename in let pretoks = prelex source in print_string reset; ===================================== src/REPL.ml ===================================== @@ -123,7 +123,7 @@ let eval_interactive in loop nodes [] [] in - let source = new Source.source_string input in + let source = Source.of_string ~label:(string_of_int i) input in let pretokens = prelex source in let tokens = lex Grammar.default_stt pretokens in (* FIXME: This is too eager: it prevents one declaration from changing the ===================================== src/debug.ml ===================================== @@ -119,10 +119,10 @@ let debug_pexp_print ptop = let debug_lexp_decls decls = let sep = " : " in List.iter (fun e -> - let ((loc, _name), lxp, _ltp) = e in + let ((sinfo, _name), lxp, _ltp) = e in + let loc = sexp_location sinfo in - printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string - (sexp_location loc)); + printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string loc); let str = lexp_str_decls (!debug_ppctx) [e] in @@ -138,7 +138,8 @@ let debug_lexp_decls decls = let str = match str with | scd :: tl - -> printf " FILE: %-25s : %s\n" (sexp_location loc).file scd; + -> let file = Source.Container.name loc.container in + printf " FILE: %-25s : %s\n" file scd; tl | _ -> [] in ===================================== src/elab.ml ===================================== @@ -1906,7 +1906,7 @@ let in_pervasive = ref true let sform_load usr_elctx loc sargs _ot = let read_file file_name elctx = - let source = new Source.source_file file_name in + let source = Source.of_path file_name in let pres = try prelex source with | Sys_error _ @@ -2003,7 +2003,7 @@ let default_ectx (* Read BTL files *) let read_file file_name elctx = - let source = new Source.source_file file_name in + let source = Source.of_path file_name in let pres = prelex source in let sxps = lex default_stt pres in let _, lctx = lexp_p_decls [] sxps elctx @@ -2060,7 +2060,7 @@ let lexp_expr_str str ctx = let tenv = default_stt in let grm = ectx_get_grammar ctx in let limit = Some ";" in - let source = new Source.source_string str in + let source = Source.of_string str in let pxps = sexp_parse_source source tenv grm limit in let lexps = lexp_parse_all pxps ctx in List.iter (fun lxp -> @@ -2071,7 +2071,7 @@ let lexp_expr_str str ctx = let lexp_decl_str str ctx = let tenv = default_stt in - let source = new Source.source_string str in + let source = Source.of_string str in let tokens = lex_source source tenv in lexp_p_decls [] tokens ctx @@ -2099,7 +2099,7 @@ let process_file : elab_context = try - let source = new Source.source_file file_name in + let source = Source.of_path file_name in let pretokens = prelex source in let tokens = lex Grammar.default_stt pretokens in let ldecls, ectx' = lexp_p_decls [] tokens ectx in ===================================== src/eval.ml ===================================== @@ -356,7 +356,7 @@ let make_float loc _depth args_val = match args_val with let make_block loc _depth args_val = match args_val with (* From what would we like to make a block? *) | [Vstring str] - -> let source = new Source.source_string str in + -> let source = Source.of_string str in Vsexp (Block (loc, (Prelexer.prelex source))) | _ -> error loc "Sexp.block expects one string as argument" ===================================== src/lexer.ml ===================================== @@ -108,7 +108,7 @@ let lex_symbol let mksym start_point escaped = if Source.Point.equal start_point source#point - then epsilon (Source.Location.of_point source#file start_point) + then epsilon (Source.Location.of_point source#container start_point) else let raw_name, location = source#slice start_point in let name = if escaped then unescape raw_name else raw_name in @@ -226,8 +226,8 @@ let lex (token_env : token_env) (pretokens : pretoken list) : sexp list = | Prestring (location, text) :: pretokens' -> loop pretokens' (String (location, text) :: acc) - | Pretoken ({file; start = {line; column; _}; _}, name) :: pretokens' - -> let source = new Source.source_string ~file ~line ~column name in + | Pretoken (location, _) :: pretokens' + -> let source = Source.of_location location in let tokens = split_presymbol token_env source in loop pretokens' (List.rev_append tokens acc) in ===================================== src/sexp.ml ===================================== @@ -113,11 +113,11 @@ let rec sexp_string ?(print_locations = false) sexp = (if print_locations then let open Source.Location in - let {file; start; end'} = sexp_location sexp + let {container; start; end'} = sexp_location sexp in Printf.sprintf "#;(\"%s\" %d %d %d %d %d %d) " - file + (Source.Container.name container) start.offset start.line start.column end'.offset end'.line end'.column else "") ===================================== src/source.ml ===================================== @@ -23,6 +23,9 @@ let first_line_of_file : int = 1 let first_column_of_line : int = 0 +let is_utf8_head (c : char) : bool = + Char.code c < 128 || Char.code c >= 192 + (** A point is a position within a source file. *) module Point = struct type t = {offset : int; line : int; column : int} @@ -60,39 +63,103 @@ module Point = struct l.offset <= r.offset end +(** A container is a thing that can hold Typer source code. *) +module Container = struct + type lines = string Array.t + + type t = + | File of string * lines (** A file can contain source code. *) + | String of string * lines (** A string entred in a REPL can contain source + code. *) + + let dummy : t = String ("<dummy>", [|""|]) + + let of_string ~(label : string) (contents : string) : t = + let lines = contents |> String.split_on_char '\n' |> Array.of_list in + String (label, lines) + + (** The name of a container is either a path or a label in the case of a + string entred in the REPL. *) + let name : t -> string = function + | File (path, _) -> path + | String (label, _) -> label + + (** The lines of source code inside the container. There is always at least + one empty line. *) + let lines : t -> string array = function + | File (_, lines) -> lines + | String (_, lines) -> lines + + (** Indexes into the lines of the text within the container. Raises + `Invalid_argument` if the index is out of bounds. *) + let nth_line (container : t) (index : int) : string = + (lines container).(index - first_line_of_file) + + (** Gets the byte at the given line and offset. Note that this is *not* the + index of the line, but its line number, which starts at 1. *) + let get (container : t) (line : int) (offset : int) : char = + let text = nth_line container line in + if String.length text = offset + then '\n' + else text.[offset] + + (** Returns the point *on* the last line, *after* the last column. *) + let end_point (self : t) : Point.t = + let lines = lines self in + let last_line = lines.(Array.length lines - 1) in + let column = + String.fold_left + (fun n c -> n + if is_utf8_head c then 1 else 0) + 0 last_line + + first_column_of_line + in + {line = Array.length lines - 1 + first_line_of_file; + column; + offset = String.length last_line} + + let equal (l : t) (r : t) : bool = + l = r +end + (** A location is an open interval of characters within a source file. *) module Location = struct - type t = {file : string; start : Point.t; end' : Point.t} + type t = {container : Container.t; start : Point.t; end' : Point.t} (** Creates a zero-width location around the given point. *) - let of_point (file : string) (point : Point.t) : t = - {file; start = point; end' = point} + let of_point (container : Container.t) (point : Point.t) : t = + {container; start = point; end' = point} (** An empty location at the beginning of an empty file. *) - let dummy = of_point "" Point.zero + let dummy = of_point Container.dummy Point.zero - let to_string (l : t) : string = - if l.start.offset = l.end'.offset - then Printf.sprintf "%s:%d:%d" l.file l.start.line l.start.column + let pp_print (f : Format.formatter) ({container; start; end'} : t) : unit = + let name = Container.name container in + if Point.equal start end' + then Format.fprintf f "%s:%d:%d" name start.line start.column else - Printf.sprintf - "%s:%d:%d-%d:%d" - l.file l.start.line l.start.column l.end'.line l.end'.column + Format.fprintf + f "%s:%d:%d-%d:%d" name start.line start.column end'.line end'.column + + let print : t -> unit = + Format.printf "%a" pp_print + + let to_string : t -> string = + Format.asprintf "%a" pp_print let equal (l : t) (r : t) = - String.equal l.file r.file + Container.equal l.container r.container && Point.equal l.start r.start && Point.equal l.end' r.end' let same (l : t) (r : t) = - String.equal l.file r.file + Container.equal l.container r.container && Point.same l.start r.start && Point.same l.end' r.end' (** Locations form a partial order where one is smaller than another iff it is entirely contained in the latter. *) let (<=) (l : t) (r : t) : bool = - if l.file <> r.file + if not (Container.equal l.container r.container) then false else Point.(<=) r.start l.start && Point.(<=) l.end' r.end' @@ -100,7 +167,7 @@ module Location = struct that covers both. If the locations do not belong to the same file, simply returns the first one. *) let extend (l : t) (r : t) : t = - if l.file <> r.file + if not (Container.equal l.container r.container) then l else if l == dummy then r @@ -109,128 +176,106 @@ module Location = struct else let start = Point.min l.start r.start in let end' = Point.max l.end' r.end' in - {file = l.file; start; end'} + {container = l.container; start; end'} end (** A source object is text paired with a cursor. The text can be lazily loaded as it is accessed byte by byte, but it must be retained for future reference by error messages. *) -class virtual t (base_line : int) (base_column : int) (file : string) = -object (self) - val mutable line = base_line - val mutable column = base_column - - (* A path if the text comes from a file, otherwise a meaningful identifier. *) - method file : string = file - - (* Return the byte at the cursor, or None if the cursor is at the end of - the text. *) - method virtual peek : char option - - (* The current point of the cursor. *) - method point : Point.t = - {offset = self#offset; line; column} - - (* The current offset of the cursor in the file, in bytes. *) - method virtual private offset : int - - (* Makes a location starting at the given point and ending at the current - cursor position. *) - method make_location (start : Point.t) : Location.t = - {file; start; end' = self#point} - - (* Slices the text, from (and including) a starting point and to (and - excluding) the curent cursor offset. - - Note that the source is required only to buffer the last line read and may - raise an Invalid_argument if the slice extends before the start of the - line. *) - method slice (point : Point.t) : string * Location.t = - (self#slice_impl point.offset, self#make_location point) - - method virtual private slice_impl : int -> string - - (* Moves the cursor forward one byte *) - method advance : unit = - let is_utf8_head c = Char.code c < 128 || Char.code c >= 192 in - let c = self#peek in - self#advance_impl; - match c with - | Some '\n' - -> line <- line + 1; - column <- 0; - | Some c when is_utf8_head c - -> column <- column + 1 - | _ -> () - - method private virtual advance_impl : unit - - (* Returns the char at the cursor, then advances it forward. *) - method next : char option = - let c = self#peek in - self#advance; - c -end - -let read_buffer_length = 4096 - -class source_file file_name = object (self) - inherit t (first_line_of_file - 1) first_column_of_line file_name - - val in_channel = open_in file_name - val mutable end_of_line = false - val mutable source_line = "" - val mutable line_offset = 0 - val mutable offset = 0 - - method private peek_unchecked = - if offset < String.length source_line - then source_line.[offset] - else '\n' - - method peek = - if offset <= String.length source_line - then Some self#peek_unchecked - else - try - line_offset <- line_offset + 1 + String.length source_line; - source_line <- input_line in_channel; - offset <- 0; - Some self#peek_unchecked - with - | End_of_file -> None - - method private advance_impl = - offset <- offset + 1 - - method private offset = line_offset + offset - - method private slice_impl start_offset = - let relative_start_offset = start_offset - line_offset in - String.sub source_line relative_start_offset (offset - relative_start_offset) -end - -class source_string - ?(file : string = "<string>") - ?(line : int = first_line_of_file) - ?(column : int = first_column_of_line) - source - = -object - inherit t line column file - - val mutable offset = 0 - - method peek = - if offset < String.length source - then Some (source.[offset]) - else None - - method private advance_impl = - offset <- offset + 1 - - method private offset = offset - - method private slice_impl start_offset = - String.sub source start_offset (offset - start_offset) -end +class t (container : Container.t) (base_point : Point.t) (end_point : Point.t) = + let line = base_point.line in + let column = base_point.column in + let offset = base_point.offset in + let end_line = end_point.line in + let end_offset = end_point.offset in + let read_cursor line offset = + if line >= end_line && offset >= end_offset + then None + else Some (Container.get container line offset) + in + object (self) + val mutable cursor = read_cursor line offset + val mutable line = line + val mutable column = column + val mutable offset = offset + + method container : Container.t = container + + (** Returns the byte at the cursor, or None if the cursor is at the end of + the text. *) + method peek : char option = + cursor + + (** The current point of the cursor. *) + method point : Point.t = + {line; column; offset} + + (** Makes a location starting at the given point and ending at the current + cursor position. *) + method make_location (start : Point.t) : Location.t = + { + container; + start; + end' = {offset; line; column}; + } + + (** Slices the text, from (and including) a starting point and to (and + excluding) the curent cursor offset. The range must be inside a single + line. *) + method slice (point : Point.t) : string * Location.t = + assert (point.line = line); + let text = Container.nth_line container line in + String.sub text point.offset (offset - point.offset), + self#make_location point + + (** Moves the cursor forward one byte. *) + method advance : unit = + match cursor with + | None -> () + | Some c + -> if c = '\n' + then begin + line <- line + 1; + column <- first_column_of_line; + offset <- 0; + end + else if is_utf8_head c + then begin + column <- column + 1; + offset <- offset + 1 + end + else + offset <- offset + 1; + cursor <- read_cursor line offset + + (** Returns the char at the cursor, then advances it forward. *) + method next : char option = + let c = self#peek in + self#advance; + c + end + +(** Creates a source object from the contents of the file at the given path. + The file is eagerly read to the end. `Sys_error` is raised if the file + cannot be openned or read. *) +let of_path (path : string) = + let channel = open_in path in + let unfold_lines () = + try Some (input_line channel, ()) with + | End_of_file -> None + in + let lines = Array.of_seq (Seq.unfold unfold_lines ()) in + close_in channel; + + let lines = if Array.length lines = 0 then [|""|] else lines in + let container = Container.File (path, lines) in + new t container Point.zero (Container.end_point container) + +let of_string ?(label : string = "<unknown>") (contents : string) = + let container = Container.of_string ~label contents in + new t container Point.zero (Container.end_point container) + +(** Creates a source object from a location. In practice, this means that the + new source will be a substring of the original source of the location. *) +let of_location (location : Location.t) : #t = + new t location.container location.start location.end' ===================================== src/string.ml ===================================== @@ -22,3 +22,12 @@ include Stdlib.String (* Backport from 5.0. *) let hash : t -> int = Hashtbl.hash + +(* Backport from 4.13. *) +let fold_left (type a) (f : a -> char -> a) (a : a) (chars : string) : a = + let rec loop n a = + if n < length chars + then loop (n + 1) (f a (get chars n)) + else a + in + loop 0 a ===================================== tests/lexer_test.ml ===================================== @@ -46,42 +46,50 @@ let test_lex name pretokens expected = in add_test "LEXER" name lex -let l os ls cs oe le ce : Source.Location.t = +let l c os ls cs oe le ce : Source.Location.t = { - file = "test.typer"; + container = c; start = {offset = os; line = ls; column = cs}; end' = {offset = oe; line = le; column = ce}; } let () = + let source = "a.b" in + let l = l (Source.Container.of_string ~label:"test" source) in test_lex "Inner operator inside a presymbol" - [Pretoken (l 0 1 0 3 1 3, "a.b")] + [Pretoken (l 0 1 0 3 1 3, source)] [Node (l 0 1 0 3 1 3, Symbol (l 1 1 1 2 1 2, "__.__"), [Symbol (l 0 1 0 1 1 1, "a"); Symbol (l 2 1 2 3 1 3, "b")])] let () = + let source = ".b" in + let l = l (Source.Container.of_string ~label:"test" source) in test_lex "Inner operators at the beginning of a presymbol" - [Pretoken (l 0 1 0 2 1 2, ".b")] + [Pretoken (l 0 1 0 2 1 2, source)] [Node (l 0 1 0 2 1 2, Symbol (l 0 1 0 1 1 1, "__.__"), [epsilon (l 0 1 0 0 1 0); Symbol (l 1 1 1 2 1 2, "b")])] let () = + let source = "a." in + let l = l (Source.Container.of_string ~label:"test" source) in test_lex "Inner operators at the end of a presymbol" - [Pretoken (l 0 1 0 2 1 2, "a.")] + [Pretoken (l 0 1 0 2 1 2, source)] [Node (l 0 1 0 2 1 2, Symbol (l 1 1 1 2 1 2, "__.__"), [Symbol (l 0 1 0 1 1 1, "a"); epsilon (l 2 1 2 2 1 2)])] let () = + let source = "." in + let l = l (Source.Container.of_string ~label:"test" source) in test_lex "An inner operator by itself is a simple symbol" - [Pretoken (l 0 1 0 1 1 1, ".")] + [Pretoken (l 0 1 0 1 1 1, source)] [Symbol (l 0 1 0 1 1 1, ".")] let () = run_all () ===================================== tests/sexp_test.ml ===================================== @@ -34,7 +34,7 @@ open Lexer open Utest_lib let sexp_parse_str dcode = - let source = new Source.source_string dcode in + let source = Source.of_string dcode in sexp_parse_source source Grammar.default_stt Grammar.default_grammar (Some ";") let test_sexp_add dcode testfun = View it on GitLab: https://gitlab.com/monnier/typer/-/compare/4421b8e7aaad4ebf4e2eb753d5bb48d3… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/4421b8e7aaad4ebf4e2eb753d5bb48d3… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Mars 2023