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

feat(base/data): fix types for cstor/select term builders

Browse source
This commit is contained in:
Simon Cruanes 2022-08-12 23:17:20 -04:00
parent e99192869d
commit 85eef2d117
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 11 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/base/Data_ty.ml
View file

@ -110,10 +110,19 @@ let data tst d : Term.t =
Term.const tst @@ Const.make (Data d) ops ~ty:(Term.type_ tst)
let cstor tst c : Term.t =
Term.const tst @@ Const.make (Cstor c) ops ~ty:(Lazy.force c.cstor_ty)
let ty_ret = Lazy.force c.cstor_ty in
let ty_args =
List.map (fun s -> Lazy.force s.select_ty) (Lazy.force c.cstor_args)
in
let ty = Term.arrow_l tst ty_args ty_ret in
Log.debugf 50 (fun k -> k "cstor %a (ty %a)" Cstor.pp c Term.pp ty);
Term.const tst @@ Const.make (Cstor c) ops ~ty
let select tst s : Term.t =
Term.const tst @@ Const.make (Select s) ops ~ty:(Lazy.force s.select_ty)
let ty_ret = Lazy.force s.select_ty in
let ty_arg = data tst s.select_cstor.cstor_ty_as_data in
let ty = Term.arrow tst ty_arg ty_ret in
Term.const tst @@ Const.make (Select s) ops ~ty
let is_a tst c : Term.t =
Term.const tst @@ Const.make (Is_a c) ops ~ty:(Term.bool tst)