diff options
Diffstat (limited to 'src/smtlib2')
| -rw-r--r-- | src/smtlib2/smtlib2_genConstr.ml | 5 | ||||
| -rw-r--r-- | src/smtlib2/smtlib2_genConstr.mli | 16 |
2 files changed, 11 insertions, 10 deletions
diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml index b320d7a..27ac8d3 100644 --- a/src/smtlib2/smtlib2_genConstr.ml +++ b/src/smtlib2/smtlib2_genConstr.ml @@ -19,6 +19,7 @@ open SmtAtom open SmtForm open SmtMisc open CoqTerms +open SmtBtype (* For debugging *) @@ -79,7 +80,7 @@ let declare_sort rt sym = let eq_refl = Term.mkProd (x,cons_t,Term.mkProd (y,cons_t,mklApp creflect [|mklApp ceq [|cons_t;rx;ry|];mklApp (lazy eq_t) [|rx;ry|]|])) in let eq_refl_v = declare_new_variable (Names.id_of_string ("eq_refl_"^s)) eq_refl in let ce = mklApp cTyp_eqb [|cons_t;eq_t;eq_refl_v|] in - let res = Btype.declare rt cons_t ce in + let res = declare rt cons_t ce in VeritSyntax.add_btype s res; res @@ -89,7 +90,7 @@ let declare_fun rt ro sym arg cod = let tyl = List.map sort_of_sort arg in let ty = sort_of_sort cod in - let coqTy = List.fold_right (fun typ c -> Term.mkArrow (Btype.interp_to_coq rt (fst typ)) c) tyl (Btype.interp_to_coq rt (fst ty)) in + let coqTy = List.fold_right (fun typ c -> Term.mkArrow (interp_to_coq rt (fst typ)) c) tyl (interp_to_coq rt (fst ty)) in let cons_v = declare_new_variable (Names.id_of_string ("Smt_var_"^s)) coqTy in let op = Op.declare ro cons_v (Array.of_list (List.map fst tyl)) (fst ty) in diff --git a/src/smtlib2/smtlib2_genConstr.mli b/src/smtlib2/smtlib2_genConstr.mli index ba69741..1aa992e 100644 --- a/src/smtlib2/smtlib2_genConstr.mli +++ b/src/smtlib2/smtlib2_genConstr.mli @@ -2,16 +2,16 @@ val pp_symbol : Smtlib2_ast.symbol -> string val string_of_symbol : Smtlib2_ast.symbol -> string val identifier_of_qualidentifier : Smtlib2_ast.qualidentifier -> Smtlib2_ast.identifier -val string_type : string -> SmtAtom.btype -val sort_of_string : string -> SmtAtom.btype * 'a list -val sort_of_symbol : Smtlib2_ast.symbol -> SmtAtom.btype * 'a list +val string_type : string -> SmtBtype.btype +val sort_of_string : string -> SmtBtype.btype * 'a list +val sort_of_symbol : Smtlib2_ast.symbol -> SmtBtype.btype * 'a list val string_of_identifier : Smtlib2_ast.identifier -> string val string_of_qualidentifier : Smtlib2_ast.qualidentifier -> string -val sort_of_sort : Smtlib2_ast.sort -> (SmtAtom.btype * 'a list as 'a) +val sort_of_sort : Smtlib2_ast.sort -> (SmtBtype.btype * 'a list as 'a) val declare_sort : - SmtAtom.Btype.reify_tbl -> Smtlib2_ast.symbol -> SmtAtom.btype + SmtBtype.reify_tbl -> Smtlib2_ast.symbol -> SmtBtype.btype val declare_fun : - SmtAtom.Btype.reify_tbl -> + SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> Smtlib2_ast.symbol -> Smtlib2_ast.sort list -> Smtlib2_ast.sort -> SmtAtom.indexed_op @@ -22,13 +22,13 @@ val make_root : SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Smtlib2_ast.term -> SmtAtom.Form.t val declare_commands : - SmtAtom.Btype.reify_tbl -> + SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> SmtAtom.Form.t list -> Smtlib2_ast.command -> SmtAtom.Form.t list val import_smtlib2 : - SmtAtom.Btype.reify_tbl -> + SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> string -> SmtAtom.Form.t list |