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">{ - &quot;keyToString&quot;: { - &quot;RunOnceActivity.OpenProjectViewOnStart&quot;: &quot;true&quot;, - &quot;RunOnceActivity.ShowReadmeOnStart&quot;: &quot;true&quot; - } -}</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@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@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@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@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@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/22282068fd8f352abaeaccf116efa1909...