simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-29 12:54:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix handling of numeral constants

Browse source
This commit is contained in:
Simon Cruanes 2022-01-04 18:18:33 -05:00
parent 691ff12a01
commit 3477f39b73
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 11 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/smtlib/Typecheck.ml
View file

@ -96,6 +96,10 @@ let is_num s =
then CCString.for_all is_digit_or_dot (String.sub s 1 (String.length s-1)) then CCString.for_all is_digit_or_dot (String.sub s 1 (String.length s-1))
else CCString.for_all is_digit_or_dot s else CCString.for_all is_digit_or_dot s
let string_as_z (s:string) : Z.t option =
try Some (Z.of_string s)
with _ -> None
let string_as_q (s:string) : Q.t option = let string_as_q (s:string) : Q.t option =
try try
let x = let x =
@ -214,10 +218,14 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
| PA.False -> T.false_ tst | PA.False -> T.false_ tst
| PA.Const s when is_num s -> | PA.Const s when is_num s ->
let open Base_types in let open Base_types in
begin match string_as_z s with
| Some n -> T.lia tst (Arith_const n)
| None ->
begin match string_as_q s with begin match string_as_q s with
| Some n -> T.lra tst (Arith_const n) | Some n -> T.lra tst (Arith_const n)
| None -> errorf_ctx ctx "expected a number for %a" PA.pp_term t | None -> errorf_ctx ctx "expected a number for %a" PA.pp_term t
end end
end
| PA.Const f | PA.Const f
| PA.App (f, []) -> | PA.App (f, []) ->
(* lookup in `let` table, then in type defs *) (* lookup in `let` table, then in type defs *)
@ -360,7 +368,6 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
A.match_ lhs cases A.match_ lhs cases
*) *)
| PA.Arith (op, l) -> | PA.Arith (op, l) ->
Log.debugf 0 (fun k->k"arith op!");
let l = List.map (conv_term ctx) l in let l = List.map (conv_term ctx) l in
conv_arith_op ctx t op l conv_arith_op ctx t op l