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

fix(typecheck): support application of function symbols

Browse source
This commit is contained in:
Simon Cruanes 2018-08-18 13:22:10 -05:00
parent ea9f374a7a
commit a88f0d62f4
1 changed files with 11 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/smtlib/Typecheck.ml
View file

@ -147,7 +147,8 @@ let rec conv_term ctx (t:PA.term) : A.term = match t with
| PA.True -> A.true_
| PA.False -> A.false_
| PA.Const s when is_num s -> A.num_str A.Ty.rat s (* numeral *)
| PA.Const f ->
| PA.Const f
| PA.App (f, []) ->
let id = find_id_ ctx f in
begin match Ctx.find_kind ctx id with
| Ctx.K_var v -> A.var v
@ -157,6 +158,15 @@ let rec conv_term ctx (t:PA.term) : A.term = match t with
| Ctx.K_cstor ty -> A.const id ty
| Ctx.K_select _ -> errorf_ctx ctx "unapplied `select` not supported"
end
| PA.App (f, args) ->
let id = find_id_ ctx f in
let args = List.map (conv_term ctx) args in
begin match Ctx.find_kind ctx id with
| Ctx.K_fun ty -> A.app (A.const id ty) args
| _ ->
(* TODO: constructor + selector *)
errorf_ctx ctx "expected constant application; got `%a`" ID.pp id
end
| PA.If (a,b,c) ->
let a = conv_term ctx a in
let b = conv_term ctx b in