From 9b99560130341673d00cd5d60e9d6039a0b9863f Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 19 Nov 2019 19:40:59 -0600 Subject: [PATCH] feat: handle typechecking and term building for datatypes --- src/base-term/Base_types.ml | 133 +++++++++++++++++--- src/base-term/Model.ml | 26 +++- src/main/main.ml | 3 +- src/smtlib/Process.ml | 28 ++--- src/smtlib/Process.mli | 1 + src/smtlib/Typecheck.ml | 203 +++++++++++++++--------------- src/smtlib/Typecheck.mli | 1 - src/smtlib/dune | 2 +- src/th-cstor/Sidekick_th_cstor.ml | 8 +- src/th-cstor/dune | 2 +- 10 files changed, 260 insertions(+), 147 deletions(-) diff --git a/src/base-term/Base_types.ml b/src/base-term/Base_types.ml index b6e06d4c..403810ed 100644 --- a/src/base-term/Base_types.ml +++ b/src/base-term/Base_types.ml @@ -26,6 +26,9 @@ and fun_ = { and fun_view = | Fun_undef of fun_ty (* simple undefined constant *) + | Fun_select of select + | Fun_cstor of cstor + | Fun_is_a of cstor | Fun_def of { pp : 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option; abs : self:term -> term IArray.t -> term * bool; (* remove the sign? *) @@ -75,12 +78,21 @@ and ty_def = and data = { data_id: ID.t; - data_cstors: (ty * select list) ID.Map.t; + data_cstors: cstor ID.Map.t lazy_t; + data_as_ty: ty lazy_t; +} + +and cstor = { + cstor_id: ID.t; + cstor_is_a: ID.t; + cstor_args: select list lazy_t; + cstor_ty_as_data: data; + cstor_ty: ty lazy_t; } and select = { - select_name: ID.t lazy_t; - select_cstor: ID.t; + select_id: ID.t; + select_cstor: cstor; select_ty: ty lazy_t; select_i: int; } @@ -96,6 +108,10 @@ and value = id: ID.t; ty: ty; } (** a named constant, distinct from any other constant *) + | V_cstor of { + c: cstor; + args: value list; + } | V_custom of { view: value_custom_view; pp: value_custom_view Fmt.printer; @@ -130,24 +146,35 @@ let id_of_fun a = a.fun_id let[@inline] eq_ty a b = a.ty_id = b.ty_id -let eq_value a b = match a, b with +let eq_cstor c1 c2 = + ID.equal c1.cstor_id c2.cstor_id + +let rec eq_value a b = match a, b with | V_bool a, V_bool b -> a=b | V_element e1, V_element e2 -> ID.equal e1.id e2.id && eq_ty e1.ty e2.ty | V_custom x1, V_custom x2 -> x1.eq x1.view x2.view - | V_bool _, _ | V_element _, _ | V_custom _, _ + | V_cstor x1, V_cstor x2 -> + eq_cstor x1.c x2.c && + CCList.equal eq_value x1.args x2.args + | (V_bool _ | V_element _ | V_custom _ | V_cstor _), _ -> false -let hash_value a = match a with +let rec hash_value a = match a with | V_bool a -> Hash.bool a | V_element e -> ID.hash e.id | V_custom x -> x.hash x.view + | V_cstor x -> + Hash.combine3 42 (ID.hash x.c.cstor_id) (Hash.list hash_value x.args) -let pp_value out = function +let rec pp_value out = function | V_bool b -> Fmt.bool out b | V_element e -> ID.pp out e.id | V_custom c -> c.pp out c.view + | V_cstor {c;args=[]} -> ID.pp out c.cstor_id + | V_cstor {c;args} -> + Fmt.fprintf out "(@[%a@ %a@])" ID.pp c.cstor_id (Util.pp_list pp_value) args let pp_db out (i,_) = Format.fprintf out "%%%d" i @@ -383,8 +410,23 @@ end = struct end module Fun : sig - type view = fun_view - type t = fun_ + type view = fun_view = + | Fun_undef of fun_ty (* simple undefined constant *) + | Fun_select of select + | Fun_cstor of cstor + | Fun_is_a of cstor + | Fun_def of { + pp : 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option; + abs : self:term -> term IArray.t -> term * bool; (* remove the sign? *) + do_cc: bool; (* participate in congruence closure? *) + relevant : 'a. ID.t -> 'a IArray.t -> int -> bool; (* relevant argument? *) + ty : ID.t -> term IArray.t -> ty; (* compute type *) + eval: value IArray.t -> value; (* evaluate term *) + } + type t = fun_ = { + fun_id: ID.t; + fun_view: fun_view; + } val id : t -> ID.t val view : t -> view @@ -394,6 +436,9 @@ module Fun : sig val as_undefined : t -> (t * Ty.Fun.t) option val as_undefined_exn : t -> t * Ty.Fun.t val is_undefined : t -> bool + val select : select -> t + val cstor : cstor -> t + val is_a : cstor -> t val do_cc : t -> bool val mk_undef : ID.t -> Ty.Fun.t -> t @@ -404,8 +449,23 @@ module Fun : sig module Map : CCMap.S with type key = t module Tbl : CCHashtbl.S with type key = t end = struct - type view = fun_view - type t = fun_ + type view = fun_view = + | Fun_undef of fun_ty (* simple undefined constant *) + | Fun_select of select + | Fun_cstor of cstor + | Fun_is_a of cstor + | Fun_def of { + pp : 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option; + abs : self:term -> term IArray.t -> term * bool; (* remove the sign? *) + do_cc: bool; (* participate in congruence closure? *) + relevant : 'a. ID.t -> 'a IArray.t -> int -> bool; (* relevant argument? *) + ty : ID.t -> term IArray.t -> ty; (* compute type *) + eval: value IArray.t -> value; (* evaluate term *) + } + type t = fun_ = { + fun_id: ID.t; + fun_view: fun_view; + } let[@inline] id t = t.fun_id let[@inline] view t = t.fun_view @@ -413,7 +473,7 @@ end = struct let as_undefined (c:t) = match view c with | Fun_undef ty -> Some (c,ty) - | Fun_def _ -> None + | Fun_def _ | Fun_cstor _ | Fun_select _ | Fun_is_a _ -> None let[@inline] is_undefined c = match view c with Fun_undef _ -> true | _ -> false @@ -424,9 +484,12 @@ end = struct let[@inline] mk_undef id ty = make id (Fun_undef ty) let[@inline] mk_undef_const id ty = mk_undef id (Ty.Fun.mk [] ty) let[@inline] mk_undef' id args ret = mk_undef id {fun_ty_args=args; fun_ty_ret=ret} + let is_a c : t = make c.cstor_is_a (Fun_is_a c) + let cstor c : t = make c.cstor_id (Fun_cstor c) + let select sel : t = make sel.select_id (Fun_select sel) let[@inline] do_cc (c:t) : bool = match view c with - | Fun_undef _ -> true + | Fun_cstor _ | Fun_select _ | Fun_undef _ | Fun_is_a _ -> true | Fun_def {do_cc;_} -> do_cc let equal a b = ID.equal a.fun_id b.fun_id @@ -580,7 +643,10 @@ end = struct )) ty_args; ty_ret + | Fun_is_a _ -> Ty.bool | Fun_def def -> def.ty f.fun_id args + | Fun_select s -> Lazy.force s.select_ty + | Fun_cstor c -> Lazy.force c.cstor_ty end let iter f view = @@ -641,6 +707,10 @@ module Term : sig val not_ : state -> t -> t val ite : state -> t -> t -> t -> t + val select : state -> select -> t -> t + val app_cstor : state -> cstor -> t IArray.t -> t + val is_a : state -> cstor -> t -> t + (** Obtain unsigned version of [t], + the sign as a boolean *) val abs : state -> t -> t * bool @@ -743,6 +813,10 @@ end = struct let[@inline] not_ st a = make st (Term_cell.not_ a) let ite st a b c : t = make st (Term_cell.ite a b c) + let select st sel t : t = app_fun st (Fun.select sel) (IArray.singleton t) + let is_a st c t : t = app_fun st (Fun.is_a c) (IArray.singleton t) + let app_cstor st c args : t = app_fun st (Fun.cstor c) args + (* might need to tranfer the negation from [t] to [sign] *) let abs tst t : t * bool = match view t with | Bool false -> true_ tst, false @@ -822,6 +896,10 @@ module Value : sig type t = value = | V_bool of bool | V_element of {id: ID.t; ty: ty} + | V_cstor of { + c: cstor; + args: value list; + } | V_custom of { view: value_custom_view; pp: value_custom_view Fmt.printer; @@ -838,6 +916,7 @@ module Value : sig val is_bool : t -> bool val is_true : t -> bool val is_false : t -> bool + val cstor_app : cstor -> t list -> t val fresh : Term.t -> t @@ -848,6 +927,10 @@ end = struct type t = value = | V_bool of bool | V_element of {id: ID.t; ty: ty} + | V_cstor of { + c: cstor; + args: value list; + } | V_custom of { view: value_custom_view; pp: value_custom_view Fmt.printer; @@ -864,6 +947,7 @@ end = struct let[@inline] is_bool = function V_bool _ -> true | _ -> false let[@inline] is_true = function V_bool true -> true | _ -> false let[@inline] is_false = function V_bool false -> true | _ -> false + let cstor_app c args : t = V_cstor {c;args} let equal = eq_value let hash = hash_value @@ -876,14 +960,28 @@ end module Data = struct type t = data = { data_id: ID.t; - data_cstors: (ty * select list) ID.Map.t; + data_cstors: cstor ID.Map.t lazy_t; + data_as_ty: ty lazy_t; } + + let pp out d = ID.pp out d.data_id +end + +module Cstor = struct + type t = cstor = { + cstor_id: ID.t; + cstor_is_a: ID.t; + cstor_args: select list lazy_t; + cstor_ty_as_data: data; + cstor_ty: ty lazy_t; + } + let equal = eq_cstor end module Select = struct type t = select = { - select_name: ID.t lazy_t; - select_cstor: ID.t; + select_id: ID.t; + select_cstor: cstor; select_ty: ty lazy_t; select_i: int; } @@ -918,6 +1016,7 @@ module Statement = struct ID.pp id (Util.pp_list Ty.pp) args Ty.pp ret | Stmt_assert t -> Fmt.fprintf out "(@[assert@ %a@])" pp_term t | Stmt_exit -> Fmt.string out "(exit)" - | Stmt_data _ -> assert false (* TODO *) + | Stmt_data l -> + Fmt.fprintf out "(@[declare-datatypes@ %a@])" (Util.pp_list Data.pp) l | Stmt_define _ -> assert false (* TODO *) end diff --git a/src/base-term/Model.ml b/src/base-term/Model.ml index 6cac8f4c..cbb1d918 100644 --- a/src/base-term/Model.ml +++ b/src/base-term/Model.ml @@ -154,12 +154,32 @@ let eval (m:t) (t:Term.t) : Value.t option = let b = aux b in if Value.equal a b then Value.true_ else Value.false_ | App_fun (c, args) -> - match Fun.view c with - | Fun_def udef -> + match Fun.view c, (args :_ IArray.t:> _ array) with + | Fun_def udef, _ -> (* use builtin interpretation function *) let args = IArray.map aux args in udef.eval args - | Fun_undef _ -> + | Fun_cstor c, _ -> + Value.cstor_app c (IArray.to_list_map aux args) + | Fun_select s, [|u|] -> + begin match aux u with + | V_cstor {c;args} when Cstor.equal c s.select_cstor -> + List.nth args s.select_i + | v_u -> + Error.errorf "cannot eval selector %a@ on %a" Term.pp t Value.pp v_u + end + | Fun_is_a c1, [|u|] -> + begin match aux u with + | V_cstor {c=c2;args=_} -> + Value.bool (Cstor.equal c1 c2) + | v_u -> + Error.errorf "cannot eval is-a %a@ on %a" Term.pp t Value.pp v_u + end + | Fun_select _, _ -> + Error.errorf "bad selector term %a" Term.pp t + | Fun_is_a _, _ -> + Error.errorf "bad is-a term %a" Term.pp t + | Fun_undef _, _ -> try Term.Map.find t m.values with Not_found -> begin match Fun.Map.find c m.funs with diff --git a/src/main/main.ml b/src/main/main.ml index dca6875e..eb7a2fae 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -108,7 +108,8 @@ let main () = let solver = let theories = [ Process.th_bool ; - ] (* TODO: more theories *) + Process.th_cstor; + ] in Process.Solver.create ~store_proof:!check ~theories tst () in diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index da8fe397..7c0cce63 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -76,10 +76,9 @@ module Check_cc = struct Stat.incr n_calls; check_conflict si c)) () - end -(* TODO +(* TODO: use external proof checker instead: check-sat(φ + model) (* check SMT model *) let check_smt_model (solver:Solver.Sat_solver.t) (hyps:_ Vec.t) (m:Model.t) : unit = Log.debug 1 "(smt.check-smt-model)"; @@ -213,8 +212,8 @@ let process_stmt (* TODO: more? *) in begin match stmt with - | Statement.Stmt_set_logic ("QF_UF"|"QF_LRA"|"QF_UFLRA") -> - E.return () (* TODO: QF_DT *) + | Statement.Stmt_set_logic ("QF_UF"|"QF_LRA"|"QF_UFLRA"|"QF_DT") -> + E.return () | Statement.Stmt_set_logic s -> Log.debugf 0 (fun k->k "warning: unknown logic `%s`" s); E.return () @@ -246,25 +245,20 @@ let process_stmt Solver.add_clause solver (IArray.singleton atom); E.return() | Statement.Stmt_data _ -> - Error.errorf "cannot deal with datatypes yet" + E.return() | Statement.Stmt_define _ -> Error.errorf "cannot deal with definitions yet" end -(* TODO: this + datatypes module Th_cstor = Sidekick_th_cstor.Make(struct - module Solver = Solver - module T = Solver.A.Term + module S = Solver + open Base_types + open Sidekick_th_cstor - let[@inline] view_as_cstor t = match view t with - | App_cst (c, args) when Fun.do_cc - | If (a,b,c) -> T_ite (a,b,c) - | Bool b -> T_bool b + let view_as_cstor t = match Term.view t with + | Term.App_fun ({fun_view=Fun.Fun_cstor _;_} as f, args) -> T_cstor (f, args) | _ -> T_other t - end - end) - *) module Th_bool = Sidekick_th_bool_static.Make(struct module S = Solver @@ -272,5 +266,5 @@ module Th_bool = Sidekick_th_bool_static.Make(struct include Form end) -let th_bool : Solver.theory = - Th_bool.theory +let th_bool : Solver.theory = Th_bool.theory +let th_cstor : Solver.theory = Th_cstor.theory diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index fcdb0b84..8b8f5972 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Process.mli @@ -8,6 +8,7 @@ module Solver and type T.Ty.t = Ty.t val th_bool : Solver.theory +val th_cstor : Solver.theory type 'a or_error = ('a, string) CCResult.t diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index 11cb10c2..fa616caa 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -26,8 +26,6 @@ module Ctx = struct type kind = | K_ty of ty_kind | K_fun of Fun.t - | K_cstor of Fun.t * Ty.t - | K_select of Fun.t * Ty.t * BT.Select.t and ty_kind = | K_atomic of Ty.def @@ -35,35 +33,24 @@ module Ctx = struct type t = { tst: T.state; - names: ID.t StrTbl.t; - kinds: kind ID.Tbl.t; + names: (ID.t * kind) StrTbl.t; lets: T.t StrTbl.t; - data: (ID.t * Ty.t) list ID.Tbl.t; (* data -> cstors *) mutable loc: Loc.t option; (* current loc *) } let create (tst:T.state) : t = { tst; names=StrTbl.create 64; - kinds=ID.Tbl.create 64; lets=StrTbl.create 16; - data=ID.Tbl.create 64; loc=None; } let loc t = t.loc let set_loc ?loc t = t.loc <- loc - let add_id_ self (s:string) (k:ID.t -> kind): ID.t = - let id = ID.make s in - StrTbl.add self.names s id; - ID.Tbl.add self.kinds id (k id); - id - - let add_id self (s:string) (k:kind): ID.t = add_id_ self s (fun _ ->k) - - let add_data self (id:ID.t) cstors: unit = - ID.Tbl.add self.data id cstors + let add_id_ self (s:string) (id:ID.t) (k:kind) : unit = + StrTbl.add self.names s (id,k); + () (* locally bind [bs] and call [f], then remove bindings *) let with_lets (self:t) (bs:(string*T.t) list) (f:unit -> 'a): 'a = @@ -72,32 +59,14 @@ module Ctx = struct ~h:(fun () -> List.iter (fun (v,_) -> StrTbl.remove self.lets v) bs) - let find_kind self (id:ID.t) : kind = - try ID.Tbl.find self.kinds id - with Not_found -> Error.errorf "did not find kind of ID `%a`" ID.pp id - - let find_ty_def self (id:ID.t) : Ty.def = - match find_kind self id with - | K_ty (K_atomic def) -> def - | _ -> Error.errorf "expected %a to be an atomic type" ID.pp id - - let as_data _self (ty:Ty.t) : BT.Data.t = - match Ty.view ty with - | Ty.Ty_atomic {def=Ty.Ty_data d;_} -> d - | _ -> Error.errorf "expected %a to be a constant type" Ty.pp ty + let find_ty_def self (s:string) : Ty.def = + match StrTbl.get self.names s with + | Some (_, K_ty (K_atomic def)) -> def + | _ -> Error.errorf "expected %s to be an atomic type" s let pp_kind out = function | K_ty _ -> Format.fprintf out "type" - | K_cstor (_,ty) -> - Format.fprintf out "(@[cstor : %a@])" Ty.pp ty - | K_select (_,ty,s) -> - Format.fprintf out "(@[select-%a-%d : %a@])" - ID.pp s.Select.select_cstor s.Select.select_i Ty.pp ty | K_fun f -> Fun.pp out f - - let pp out t = - Format.fprintf out "ctx {@[%a@]}" - Fmt.(seq ~sep:(return "@ ") @@ pair ID.pp pp_kind) (ID.Tbl.to_seq t.kinds) end let error_loc ctx : string = Fmt.sprintf "at %a: " pp_loc_opt (Ctx.loc ctx) @@ -112,7 +81,7 @@ let check_bool_ ctx t = ill_typed ctx "expected bool, got `@[%a : %a@]`" T.pp t Ty.pp (T.ty t) ) -let find_id_ ctx (s:string): ID.t = +let find_id_ ctx (s:string): ID.t * Ctx.kind = try StrTbl.find ctx.Ctx.names s with Not_found -> errorf_ctx ctx "name `%s` not in scope" s @@ -131,7 +100,7 @@ let rec conv_ty ctx (t:PA.ty) : Ty.t = match t with ill_typed ctx "cannot handle ints for now" (* TODO: A.Ty.int , Ctx.K_ty Ctx.K_other *) | PA.Ty_app (f, l) -> - let def = Ctx.find_ty_def ctx @@ find_id_ ctx f in + let def = Ctx.find_ty_def ctx f in let l = List.map (conv_ty ctx) l in Ty.atomic def l | PA.Ty_arrow _ -> @@ -158,25 +127,18 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t = begin match StrTbl.find ctx.Ctx.lets f with | u -> u | exception Not_found -> - let id = find_id_ ctx f in - begin match Ctx.find_kind ctx id with - | Ctx.K_fun f -> T.const tst f - | Ctx.K_ty _ -> - errorf_ctx ctx "expected term, not type; got `%a`" ID.pp id - | Ctx.K_cstor _ -> - errorf_ctx ctx "cannot handle constructors for now" - (* FIXME: A.const id ty *) - | Ctx.K_select _ -> errorf_ctx ctx "unapplied `select` not supported" + begin match find_id_ ctx f with + | _, Ctx.K_fun f -> T.const tst f + | _, Ctx.K_ty _ -> + errorf_ctx ctx "expected term, not type; got `%s`" f end 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 f -> T.app_fun tst f (IArray.of_list args) - | _ -> - (* TODO: constructor + selector *) - errorf_ctx ctx "expected constant application; got `%a`" ID.pp id + begin match find_id_ ctx f with + | _, Ctx.K_fun f -> T.app_fun tst f (IArray.of_list args) + | _, Ctx.K_ty _ -> + errorf_ctx ctx "expected function, got type `%s` instead" f end | PA.If (a,b,c) -> let a = conv_term ctx a in @@ -214,6 +176,13 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t = let a = conv_term ctx a in let b = conv_term ctx b in Form.imply tst a b + | PA.Is_a (s, u) -> + let u = conv_term ctx u in + begin match find_id_ ctx s with + | _, Ctx.K_fun {Fun.fun_view=Fun_cstor c; _} -> + Term.is_a tst c u + | _ -> errorf_ctx ctx "expected `%s` to be a constructor" s + end | PA.Match (_lhs, _l) -> errorf_ctx ctx "TODO: support match in %a" PA.pp_term t (* FIXME: do that properly, using [with_lets] with selectors @@ -370,19 +339,20 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list = | PA.Stmt_set_info (a,b) -> [Stmt.Stmt_set_info (a,b)] | PA.Stmt_exit -> [Stmt.Stmt_exit] | PA.Stmt_decl_sort (s,n) -> - let id = Ctx.add_id_ ctx s - (fun id -> Ctx.K_ty (Ctx.K_atomic (Ty.Ty_uninterpreted id))) in + let id = ID.make s in + Ctx.add_id_ ctx s id + (Ctx.K_ty (Ctx.K_atomic (Ty.Ty_uninterpreted id))); [Stmt.Stmt_ty_decl (id, n)] | PA.Stmt_decl fr -> let f, args, ret = conv_fun_decl ctx fr in - let id = Ctx.add_id_ ctx f - (fun id -> Ctx.K_fun (Fun.mk_undef' id args ret)) in + let id = ID.make f in + Ctx.add_id_ ctx f id + (Ctx.K_fun (Fun.mk_undef' id args ret)); [Stmt.Stmt_decl (id, args,ret)] - | PA.Stmt_data l when List.for_all (fun ((_,n),_) -> n=0) l -> - errorf_ctx ctx "cannot typecheck datatypes" - (* FIXME + | PA.Stmt_data l -> (* first, read and declare each datatype (it can occur in the other datatypes' constructors) *) + (* TODO:remove let pre_parse ((data_name,arity),cases) = if arity <> 0 then ( errorf_ctx ctx "cannot handle polymorphic datatype %s" data_name; @@ -391,48 +361,77 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list = data_id, cases in let l = List.map pre_parse l in + *) + let module Cstor = Base_types.Cstor in + let cstors_of_data data (cstors:PA.cstor list) : Cstor.t ID.Map.t = + let parse_case {PA.cstor_name; cstor_args; cstor_ty_vars} = + if cstor_ty_vars <> [] then ( + errorf_ctx ctx "cannot handle polymorphic constructor %s" cstor_name; + ); + let cstor_id = ID.make cstor_name in + (* how to translate selectors *) + let mk_selectors (cstor:Cstor.t) = + List.mapi + (fun i (name,ty) -> + let select_id = ID.make name in + let sel = { + Select. + select_id; + select_ty=lazy (conv_ty ctx ty); + select_cstor=cstor; + select_i=i; + } in + (* now declare the selector *) + Ctx.add_id_ ctx name select_id + (Ctx.K_fun (Fun.select sel)); + sel) + cstor_args + in + let rec cstor = { + Cstor. + cstor_id; + cstor_is_a = ID.makef "is-a.%s" cstor_name; (* every fun needs a name *) + cstor_args=lazy (mk_selectors cstor); + cstor_ty_as_data=data; + cstor_ty=data.data_as_ty; + } in + (* declare cstor *) + Ctx.add_id_ ctx cstor_name cstor_id (Ctx.K_fun (Fun.cstor cstor)); + cstor_id, cstor + in + let cstors = List.map parse_case cstors in + ID.Map.of_list cstors + in (* now parse constructors *) let l = List.map - (fun (data_id, (cstors:PA.cstor list)) -> - let data_ty = Ty.const data_id in - let parse_case {PA.cstor_name=c; cstor_args; cstor_ty_vars} = - if cstor_ty_vars <> [] then ( - errorf_ctx ctx "cannot handle polymorphic constructor %s" c; + (fun ((data_name,arity), (cstors:PA.cstor list)) -> + if arity <> 0 then ( + (* TODO: handle poly datatypes properly *) + errorf_ctx ctx "cannot handle polymorphic datatype %s" data_name; + ); + let data_id = ID.make data_name in + let rec data = { + Data. + data_id; + data_cstors=lazy (cstors_of_data data cstors); + data_as_ty=lazy ( + let def = Ty.Ty_data data in + Ty.atomic def [] ); - let selectors = - List.map (fun (n,ty) -> Some n, conv_ty_fst ctx ty) cstor_args - in - let ty_args = List.map snd selectors in - (* declare cstor *) - let ty_c = Ty.arrow_l ty_args data_ty in - let id_c = Ctx.add_id ctx c (Ctx.K_cstor ty_c) in - (* now declare selectors *) - List.iteri - (fun i (name_opt,ty) -> match name_opt with - | None -> () - | Some select_str -> - (* declare this selector *) - let rec select_name = lazy - (Ctx.add_id ctx select_str - (Ctx.K_select (ty, - {A.select_name; select_cstor=id_c; select_i=i}))) - in - ignore (Lazy.force select_name)) - selectors; - (* return cstor *) - id_c, ty_c - in - let cstors = List.map parse_case cstors in - (* update info on [data] *) - Ctx.add_data ctx data_id cstors; - {Ty.data_id; data_cstors=ID.Map.of_list cstors}) + } in + Ctx.add_id_ ctx data_name data_id + (Ctx.K_ty (Ctx.K_atomic (Ty.Ty_data data))); + data) l in - [A.Data l] - *) - | PA.Stmt_data _ -> - errorf_ctx ctx "not implemented: parametric datatypes" PA.pp_stmt stmt + (* now force definitions *) + List.iter + (fun {Data.data_cstors=lazy m;data_as_ty=lazy _;_} -> + ID.Map.iter (fun _ {Cstor.cstor_args=lazy _;_} -> ()) m; + ()) + l; + [Stmt.Stmt_data l] | PA.Stmt_funs_rec _defs -> errorf_ctx ctx "not implemented: definitions" PA.pp_stmt stmt (* TODO @@ -447,9 +446,9 @@ and conv_statement_aux ctx (stmt:PA.statement) : Stmt.t list = {PA.fr_decl={PA.fun_ty_vars=[]; fun_args=[]; fun_name; fun_ret}; fr_body} -> (* turn [def f : ret := body] into [decl f : ret; assert f=body] *) let ret = conv_ty ctx fun_ret in - let id = Ctx.add_id_ ctx fun_name - (fun id -> Ctx.K_fun (Fun.mk_undef_const id ret)) in - let f = match Ctx.find_kind ctx id with Ctx.K_fun f->f | _ -> assert false in + let id = ID.make fun_name in + let f = Fun.mk_undef_const id ret in + Ctx.add_id_ ctx fun_name id (Ctx.K_fun f); let rhs = conv_term ctx fr_body in [ Stmt.Stmt_decl (id,[],ret); Stmt.Stmt_assert (Form.eq tst (T.const tst f) rhs); diff --git a/src/smtlib/Typecheck.mli b/src/smtlib/Typecheck.mli index d5dbfafa..ca0caf72 100644 --- a/src/smtlib/Typecheck.mli +++ b/src/smtlib/Typecheck.mli @@ -14,7 +14,6 @@ type 'a or_error = ('a, string) CCResult.t module Ctx : sig type t val create: T.state -> t - val pp : t CCFormat.printer end val conv_term : Ctx.t -> PA.term -> T.t diff --git a/src/smtlib/dune b/src/smtlib/dune index 9913fdde..36d4e020 100644 --- a/src/smtlib/dune +++ b/src/smtlib/dune @@ -3,7 +3,7 @@ (public_name sidekick-bin.smtlib) (libraries containers zarith msat sidekick.core sidekick.util sidekick.msat-solver sidekick.base-term sidekick.th-bool-static - sidekick.mini-cc msat.backend smtlib-utils) + sidekick.mini-cc sidekick.th-cstor msat.backend smtlib-utils) (flags :standard -warn-error -27-37 -open Sidekick_util)) ; TODO: enable warn-error again diff --git a/src/th-cstor/Sidekick_th_cstor.ml b/src/th-cstor/Sidekick_th_cstor.ml index 2235fb29..58dc9642 100644 --- a/src/th-cstor/Sidekick_th_cstor.ml +++ b/src/th-cstor/Sidekick_th_cstor.ml @@ -1,7 +1,7 @@ (** {1 Theory for constructors} *) type ('c,'t) cstor_view = - | T_cstor of 'c * 't list + | T_cstor of 'c * 't IArray.t | T_other of 't let name = "th-cstor" @@ -28,7 +28,7 @@ module Make(A : ARG) : S with module A = A = struct t: T.t; n: N.t; cstor: Fun.t; - args: T.t list; + args: T.t IArray.t; } (* associate to each class a unique constructor term in the class (if any) *) @@ -65,8 +65,8 @@ module Make(A : ARG) : S with module A = A = struct in if Fun.equal cr1.cstor cr2.cstor then ( (* same function: injectivity *) - assert (List.length cr1.args = List.length cr2.args); - List.iter2 + assert (IArray.length cr1.args = IArray.length cr2.args); + IArray.iter2 (fun u1 u2 -> SI.CC.merge_t cc u1 u2 expl) cr1.args cr2.args ) else ( diff --git a/src/th-cstor/dune b/src/th-cstor/dune index b4e89620..051c7e9b 100644 --- a/src/th-cstor/dune +++ b/src/th-cstor/dune @@ -1,7 +1,7 @@ (library (name Sidekick_th_cstor) - (public_name sidekick.smt.th-cstor) + (public_name sidekick.th-cstor) (libraries containers sidekick.core sidekick.util) (flags :standard -open Sidekick_util))