From a88f0d62f46fda9fce901e4eaea71f3fc795478e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 18 Aug 2018 13:22:10 -0500 Subject: [PATCH] fix(typecheck): support application of function symbols --- src/smtlib/Typecheck.ml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index aec2f0e1..36238be0 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -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