Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found
Select Git revision
  • SimonJ
  • add-proj
  • alice
  • case-unification
  • compiler-phase-simpl
  • dev/characterization
  • diagnostics_and_hover
  • feedback/graveline
  • gambit-compile-pervasives
  • gensym-without-spaces
  • instance-args
  • ja--elab-flamecharts
  • ja-barszcz
  • ja-perf
  • ja-refl
  • laurent/elab_cache
  • location-sinfo
  • main
  • master
  • misc-bugfixes
  • ocaml-toplevel
  • open-module
  • quot-types/normalisation
  • quot-types/rational
  • report/hmdup
  • report/itd
  • report/jfla-2019
  • report/ml-2017
  • report/tcvi
  • report/vincent-bonnevalle
  • residue-fix
  • residues-elab
  • sexp-case
  • simon--logging-overhaul
  • simon--pp-print-lctx
  • simon--pp-print-value
  • simon--remove-heap
  • simon--trace-evaluation-through-logging
  • there-can-be-only-one-inductive
  • tp/ift6172
  • trace-vs-diagnose
  • track-sexp-lexp
  • typer-lsp-server
43 results

Target

Select target project
  • monnier/typer
  • league/typer
  • jamestjw/typer
  • rdivyanshu/typer
  • jabarszcz/typer
  • JasonHuZS/typer
  • npereira97/typer
  • hannelita/typer
  • khaledPac/typer
  • shonfeder/typer
10 results
Select Git revision
  • SimonJ
  • add-proj
  • alice
  • case-unification
  • compiler-phase-simpl
  • dev/characterization
  • diagnostics_and_hover
  • feedback/graveline
  • gambit-compile-pervasives
  • gensym-without-spaces
  • instance-args
  • ja--elab-flamecharts
  • ja-barszcz
  • ja-perf
  • ja-refl
  • laurent/elab_cache
  • location-sinfo
  • main
  • master
  • misc-bugfixes
  • ocaml-toplevel
  • open-module
  • quot-types/normalisation
  • quot-types/rational
  • report/hmdup
  • report/itd
  • report/jfla-2019
  • report/ml-2017
  • report/tcvi
  • report/vincent-bonnevalle
  • residue-fix
  • residues-elab
  • sexp-case
  • simon--logging-overhaul
  • simon--pp-print-lctx
  • simon--pp-print-value
  • simon--remove-heap
  • simon--trace-evaluation-through-logging
  • there-can-be-only-one-inductive
  • tp/ift6172
  • trace-vs-diagnose
  • track-sexp-lexp
  • typer-lsp-server
43 results
Show changes
Commits on Source (4)
Expand all Show whitespace changes
Inline Side-by-side
Showing
with 1305 additions and 1556 deletions
.idea/workspace.xml deleted 100644 → 0
View file @ ad1d941d
<?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
View file @ 65e931bd
......@@ -38,72 +38,23 @@ open Debruijn
open Fmt
let input_paths = ref []
let format_mode = ref false
let ppctx = ref Lexp.ppctx
let output_path = ref None
let typecheck = ref false
let pretok = ref false
let tok = ref false
let pexp = ref false
let lexp = ref false
let lctx = ref false
let print_rctx = ref false
let arg_defs =
[
("--format",
Arg.Unit (fun () -> format_mode := true),
" format a typer source code");
("-fmt-pretty=on",
Arg.Unit (fun () -> ppctx := {!ppctx with pretty = true}),
" Print with indentation");
("-fmt-pretty=off",
Arg.Unit (fun () -> ppctx := {!ppctx with pretty = false}),
" Print expression in one line");
("-fmt-type=on",
Arg.Unit (fun () -> ppctx := {!ppctx with print_type = true}),
" Print type info");
("-fmt-type=off",
Arg.Unit (fun () -> ppctx := {!ppctx with print_type = false}),
" Don't print type info");
("-fmt-index=on",
Arg.Unit (fun () -> ppctx := {!ppctx with print_dbi = true}),
" Print DBI index");
("-fmt-index=off",
Arg.Unit (fun () -> ppctx := {!ppctx with print_dbi = false}),
" Don't print DBI index");
("-fmt-indent-size",
Arg.Int (fun i -> ppctx := {!ppctx with indent_size = i}),
" Indent size");
("-fmt-highlight=on",
Arg.Unit (fun () -> ppctx := {!ppctx with color = true}),
" Enable Highlighting for typer code");
("-fmt-highlight=off",
Arg.Unit (fun () -> ppctx := {!ppctx with color = false}),
" Disable Highlighting for typer code");
("-fmt-file",
Arg.String (fun path -> output_path := Some path),
" Output formatted code to a file");
("-typecheck",
Arg.Unit (fun () -> typecheck := true),
" Enable type checking");
(* Debug *)
("-pretok", Arg.Unit (fun () -> pretok := true), " Print pretok debug info");
("-tok", Arg.Unit (fun () -> tok := true), " Print tok debug info");
("-pexp", Arg.Unit (fun () -> pexp := true), " Print pexp debug info");
("-lexp", Arg.Unit (fun () -> lexp := true), " Print lexp debug info");
("-lctx", Arg.Unit (fun () -> lctx := true), " Print lexp context");
("-rctx", Arg.Unit (fun () -> print_rctx := true), " Print runtime context");
("-all",
Arg.Unit
(fun ()
-> pretok := true;
tok := true;
pexp := true;
lexp := true;
lctx := true;
-> lctx := true;
print_rctx := true),
" Print all debug info");
]
......@@ -111,74 +62,15 @@ let arg_defs =
let parse_args () =
Arg.parse arg_defs (fun path -> input_paths := path :: !input_paths) ""
let format_source () =
print_string (make_title " ERRORS ");
let filename = List.hd (!input_paths) in
let source = new Source.source_file filename in
let pretoks = Prelexer.prelex source in
let toks = Lexer.lex Grammar.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.lexp_str_decls (!ppctx) (List.flatten lexps) in
match !output_path with
| Some output_path
-> ppctx := {!ppctx with color = false};
printf " Writing output file: %s\n" output_path;
let file = open_out output_path in
Fun.protect
~finally:(fun () -> close_out file)
(fun () -> List.iter (fun str -> output_string file str) result)
| None -> List.iter print_endline result
let main () =
parse_args ();
if Array.length Sys.argv == 1
then
Arg.usage
(Arg.align arg_defs)
(sprintf "\n Usage: %s <file_name> [options]\n" Sys.argv.(0))
else if !format_mode
then format_source ()
else
begin
if not (!pretok || !tok || !pexp || !lexp || !lctx || !print_rctx) then
begin
pexp := true;
lexp := true;
end;
let debug_pipeline () =
try
if not (!lctx || !print_rctx) then
lctx := true;
let filename = List.hd !input_paths in
(* get pretokens*)
print_string yellow;
let source = new Source.source_file filename in
let pretoks = Prelexer.prelex source in
print_string reset;
if !pretok then
begin
print_string (make_title " PreTokens");
Debug.debug_pretokens_print_all pretoks;
print_string "\n"
end;
(* get sexp/tokens *)
print_string yellow;
let toks = Lexer.lex Grammar.default_stt pretoks in
print_string reset;
if !tok then
begin
print_string (make_title " Base Sexp");
Debug.debug_sexp_print_all toks;
print_string "\n"
end;
(* get lexp *)
let octx = Elab.default_ectx in
......@@ -208,13 +100,6 @@ let main () =
print_endline (" " ^ (make_line '-' 76));
end;
if !lexp then
begin
print_string (make_title " Lexp ");
Debug.debug_lexp_decls flexps;
print_string "\n"
end;
if !lctx then
begin
print_lexp_ctx (ectx_to_lctx nctx);
......@@ -261,6 +146,19 @@ let main () =
Eval.print_eval_result 1 body
with
| Not_found -> ()
end
with
| Log.Stop_compilation (message)
-> printf "%s" message;
Log.print_log ()
let main () =
parse_args ();
if Array.length Sys.argv == 1
then
Arg.usage
(Arg.align arg_defs)
(sprintf "\n Usage: %s <file_name> [options]\n" Sys.argv.(0))
else debug_pipeline ()
let _ = main ()
src/debruijn.ml
View file @ 65e931bd
......@@ -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.output 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 100644 → 0
View file @ ad1d941d
(*
* 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(f, args)
-> print_info "Node: " (sexp_location f);
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 ((loc, _name), lxp, _ltp) = e in
printf "%-15s[%s]" (lexp_name lxp) (Source.Location.to_string
(sexp_location 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
-> printf " FILE: %-25s : %s\n" (sexp_location loc).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
View file @ 65e931bd
This diff is collapsed.
src/elexp.ml
View file @ 65e931bd
......@@ -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
| Type of Lexp.lexp
let rec elexp_location e =
match e with
| Imm s -> sexp_location s
| Var ((l,_), _) -> sexp_location l
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,_) -> elexp_location f
| Lambda ((l,_),_) -> Sexp.location l
| Call (f, _) -> location f
| Cons (_, (l, _)) -> l
| Case (l,_,_,_) -> l
| Type e -> L.lexp_location e
| Type e -> Lexp.lexp_location e
let elexp_name 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" Sexp.pp_print_symbol 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
View file @ 65e931bd
......@@ -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
let value_location : value_type -> Source.Location.t = function
| Vcons ((loc, _), _) -> loc
| Closure (_, lxp, _) -> elexp_location lxp
| Closure (_, lxp, _) -> Elexp.location lxp
(* location info was lost or never existed *)
| _ -> dloc
| _ -> 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
View file @ 65e931bd
......@@ -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
......@@ -110,7 +106,7 @@ 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
View file @ 65e931bd
......@@ -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
View file @ 65e931bd
......@@ -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
View file @ 65e931bd
......@@ -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
......@@ -219,5 +230,5 @@ let resolve_instances instantiate_implicit e =
| _ ->
Log.log_error ~loc:(L.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
View file @ 65e931bd
......@@ -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/lexp.ml
View file @ 65e931bd
This diff is collapsed.
src/listx.ml → src/list.ml
View file @ 65e931bd
......@@ -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
View file @ 65e931bd
This diff is collapsed.
src/pexp.ml
View file @ 65e931bd
......@@ -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
......@@ -58,12 +68,13 @@ 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
| _
-> 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 pname = Symbol (sexp_location l, match oname with None -> "_" | Some n -> n) in
let pname = Symbol (Sexp.location l, match oname with None -> "_" | Some n -> n) in
match okn with
| None -> pname
| Some ((l,_) as n) ->
......@@ -73,10 +84,11 @@ let pexp_p_pat (s : sexp) : ppat = match s with
| Symbol (_l, n) -> Ppatsym (s, match n with "_" -> None | _ -> Some n)
| Node (c, args)
-> Ppatcons (c, List.map pexp_p_pat_arg args)
| _ -> let l = sexp_location s in
| _
-> 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)
| Ppatsym (l, None) -> Symbol (Sexp.location l, "_")
| Ppatsym (l, Some n) -> Symbol (Sexp.location l, n)
| Ppatcons (c, args) -> Node (c, List.map pexp_u_pat_arg args)
src/prelexer.ml
View file @ 65e931bd
......@@ -40,8 +40,25 @@ module Pretoken = struct
| 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
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 +202,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
View file @ 65e931bd
(* 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.
......@@ -30,6 +30,9 @@ let sexp_error ?print_action loc fmt =
type integer = Z.t
type symbol = location * string
let pp_print_symbol (f : Format.formatter) (_, name : symbol) : unit =
Format.pp_print_string f name
type sexp = (* Syntactic expression, kind of like Lisp. *)
| Block of location * pretoken list
| Symbol of symbol
......@@ -47,6 +50,16 @@ 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 =
......@@ -72,40 +85,43 @@ let emptyString = hString ""
(*************** The Sexp Printer *********************)
let rec sexp_location (s : sexp) : location =
let rec location (s : sexp) : location =
match s with
| Block (l, _) -> l
| Symbol (l, _) -> l
| String (l, _) -> l
| Integer (l, _) -> l
| Float (l, _) -> l
| Node (s, _) -> sexp_location s
(* 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 {file; start_line; start_column; end_line; end_column} =
sexp_location sexp
in
Printf.sprintf
"#;(\"%s\" %d %d %d %d) " file start_line start_column 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)
| Node (s, _) -> location s
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
......@@ -259,7 +275,7 @@ 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
......
src/source.ml
View file @ 65e931bd
......@@ -57,6 +57,27 @@ module Location = struct
end_column = column;
}
let pp_print_long (f : Format.formatter) (location : t) =
if
location.start_line = location.end_line
&& location.start_column = location.end_column
then
Format.fprintf
f
"[%s:%d:%d]"
location.file
location.start_line
location.start_column
else
Format.fprintf
f
"[%s:%d:%d-%d:%d]"
location.file
location.start_line
location.start_column
location.end_line
location.end_column
let to_string
({file; start_line; start_column; end_line; end_column} : t)
: string =
......@@ -94,6 +115,33 @@ module Location = struct
&& Int.equal l_end_column r_end_column
end
type Format.stag += Located of Location.t
let pp_enable_print_locations
(f : Format.formatter)
(pp_print_location : Format.formatter -> Location.t -> unit)
: 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@ " pp_print_location 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
(* Traditionally, line numbers start at 1… *)
let first_line_of_file = 1
(* … and so do column numbers :-( *)
......
src/unification.ml
View file @ 65e931bd
......@@ -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
......