simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-05 19:00:33 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor: adapt to new levels in core

Browse source
This commit is contained in:
Simon Cruanes 2023-02-23 22:07:55 -05:00
parent b8cbe0cf06
commit 9ea96a6b61
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
3 changed files with 11 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/core/t_printer.ml
View file

@ -45,8 +45,8 @@ let expr_pp_with_ ~max_depth ~max_nodes ~hooks out (e : term) : unit =
let hook_fired = List.exists (fun h -> h ~recurse:pp' out e) hooks in
if not hook_fired then (
match Term.view e with
| E_type 0 -> Fmt.string out "Type"
| E_type i -> Fmt.fprintf out "Type(%d)" i
| E_type lvl when Level.is_one lvl -> Fmt.string out "Type"
| E_type lvl -> Fmt.fprintf out "Type.{%a}" Level.pp lvl
| E_var v -> Fmt.string out (Var.name v)
(* | E_var v -> Fmt.fprintf out "(@[%s : %a@])" v.v_name pp v.v_ty *)
| E_bound_var v ->

8
src/core/t_trace_reader.ml
View file

@ -54,8 +54,12 @@ let decode_term (self : t) ~read_subterm ~tag : Term.t Dec.t =
Term.app self.tst f a)
| "Ty" ->
Dec.(
let+ i = int in
Term.type_of_univ self.tst i)
let* lvl = string in
(match int_of_string_opt lvl with
| Some i -> return @@ Term.type_of_univ_int self.tst i
| None ->
(* FIXME: parse/deserialize the level here *)
failf "cannot parse level %S" lvl))
| "Tl" ->
Dec.(
let+ v, ty, bod = tup3 string read_subterm read_subterm in

4
src/core/t_tracer.ml
View file

@ -17,7 +17,9 @@ let emit_term_ (self : state) (t : Term.t) =
| T.E_var v -> "TV", V.(list [ string (Var.name v); loop' v.v_ty ])
| T.E_bound_var v -> "Tv", V.(list [ int (Bvar.idx v); loop' v.bv_ty ])
| T.E_app (f, a) -> "T@", V.(list [ loop' f; loop' a ])
| T.E_type i -> "Ty", V.int i
| T.E_type lvl ->
(* FIXME: actually serialize level *)
"Ty", V.string (Level.to_string lvl)
| T.E_const ({ Const.c_ty; _ } as const) ->
let tag, view = Const.ser ~ser_t:loop' const in
( "Tc",