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

Removed additional libs.

Browse source
This commit is contained in:
Guillaume Bury 2016-09-12 15:32:22 +02:00
parent 9d509241ad
commit dfff903f8c
10 changed files with 725 additions and 710 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
Makefile
View file

@ -10,15 +10,15 @@ TEST_BIN=tests/test_api.native
NAME_OCAMLFIND=msat
NAME_BIN=msat
NAME_CORE=msat
NAME_SAT=msat_sat
NAME_SMT=msat_smt
NAME_MCSAT=msat_mcsat
#NAME_SAT=msat_sat
#NAME_SMT=msat_smt
#NAME_MCSAT=msat_mcsat
LIB_CORE=$(addprefix $(NAME_CORE), .cma .cmxa .cmxs)
LIB_SAT=$(addprefix $(NAME_SAT), .cma .cmxa .cmxs)
LIB_SMT=$(addprefix $(NAME_SMT), .cma .cmxa .cmxs)
LIB_MCSAT=$(addprefix $(NAME_MCSAT), .cma .cmxa .cmxs)
LIB=$(LIB_CORE) $(LIB_SAT) # $(LIB_SMT) $(LIB_MCSAT)
#LIB_SAT=$(addprefix $(NAME_SAT), .cma .cmxa .cmxs)
#LIB_SMT=$(addprefix $(NAME_SMT), .cma .cmxa .cmxs)
#LIB_MCSAT=$(addprefix $(NAME_MCSAT), .cma .cmxa .cmxs)
LIB=$(LIB_CORE) # $(LIB_SAT) $(LIB_SMT) $(LIB_MCSAT)
all: lib test
@ -28,7 +28,7 @@ lib:
doc:
$(COMP) $(FLAGS) $(DOC)
bin: lib
bin:
$(COMP) $(FLAGS) $(BIN)
cp $(BIN) $(NAME_BIN) && rm $(BIN)

151
src/main.ml
View file

@ -4,10 +4,11 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
module Sat = Msat_sat.Sat.Make(struct end)
module Sat = Sat.Make(struct end)
module Dummy = Sat
(*
module Smt = Msat_smt.Smt.Make(struct end)
module Mcsat = Msat_smt.Mcsat.Make(struct end)
module Smt = Smt.Make(struct end)
module Mcsat = Mcsat.Make(struct end)
*)
module P =
@ -99,7 +100,7 @@ let argspec = Arg.align [
"<t>[smhd] Sets the time limit for the sat solver";
"-u", Arg.Set p_unsat_core,
" Prints the unsat-core explanation of the unsat proof (if used with -check)";
"-v", Arg.Int (fun i -> Msat.Log.set_debug i),
"-v", Arg.Int (fun i -> Log.set_debug i),
"<lvl> Sets the debug verbose level";
]
@ -113,28 +114,30 @@ let check () =
else if s > !size_limit then
raise Out_of_space
let do_task
(module S : Msat.External.S
with type St.formula = Msat.Expr.atom) s =
match s.Dolmen.Statement.descr with
| Dolmen.Statement.Def (id, t) -> Type.new_def id t
| Dolmen.Statement.Decl (id, t) -> Type.new_decl id t
| Dolmen.Statement.Consequent t ->
let f = Type.new_formula t in
let cnf = Msat.Expr.Formula.make_cnf f in
S.assume cnf
| Dolmen.Statement.Antecedent t ->
let f = Msat.Expr.Formula.make_not @@ Type.new_formula t in
let cnf = Msat.Expr.Formula.make_cnf f in
S.assume cnf
| Dolmen.Statement.Prove ->
begin match S.solve () with
| S.Sat _ -> ()
| S.Unsat _ -> ()
end
| _ ->
Format.printf "Command not supported:@\n%a@."
Dolmen.Statement.print s
module Make
(T : Type.S)
(S : External.S with type St.formula = T.atom) = struct
let do_task s =
match s.Dolmen.Statement.descr with
| Dolmen.Statement.Def (id, t) -> T.def id t
| Dolmen.Statement.Decl (id, t) -> T.decl id t
| Dolmen.Statement.Consequent t ->
let cnf = T.consequent t in
S.assume cnf
| Dolmen.Statement.Antecedent t ->
let cnf = T.antecedent t in
S.assume cnf
| Dolmen.Statement.Prove ->
begin match S.solve () with
| S.Sat _ -> ()
| S.Unsat _ -> ()
end
| _ ->
Format.printf "Command not supported:@\n%a@."
Dolmen.Statement.print s
end
let main () =
(* Administrative duties *)
@ -150,55 +153,55 @@ let main () =
Gc.delete_alarm al;
()
(* Old code ...
(* Old code ...
let cnf = get_cnf () in
if !p_cnf then
print_cnf cnf;
match !solver with
| Smt ->
Smt.assume cnf;
let res = Smt.solve () in
Gc.delete_alarm al;
begin match res with
| Smt.Sat sat ->
let t = Sys.time () in
if !p_check then
if not (List.for_all (List.exists sat.Solver_intf.eval) cnf) then
raise Incorrect_model;
print "Sat (%f/%f)" t (Sys.time () -. t)
| Smt.Unsat us ->
let t = Sys.time () in
if !p_check then begin
let p = us.Solver_intf.get_proof () in
Smt.Proof.check p;
print_proof p;
if !p_unsat_core then
print_unsat_core (Smt.unsat_core p)
end;
print "Unsat (%f/%f)" t (Sys.time () -. t)
end
| Mcsat ->
Mcsat.assume cnf;
let res = Mcsat.solve () in
begin match res with
| Mcsat.Sat sat ->
let t = Sys.time () in
if !p_check then
if not (List.for_all (List.exists sat.Solver_intf.eval) cnf) then
raise Incorrect_model;
print "Sat (%f/%f)" t (Sys.time () -. t)
| Mcsat.Unsat us ->
let t = Sys.time () in
if !p_check then begin
let p = us.Solver_intf.get_proof () in
Mcsat.Proof.check p;
print_mcproof p;
if !p_unsat_core then
print_mc_unsat_core (Mcsat.unsat_core p)
end;
print "Unsat (%f/%f)" t (Sys.time () -. t)
end
let cnf = get_cnf () in
if !p_cnf then
print_cnf cnf;
match !solver with
| Smt ->
Smt.assume cnf;
let res = Smt.solve () in
Gc.delete_alarm al;
begin match res with
| Smt.Sat sat ->
let t = Sys.time () in
if !p_check then
if not (List.for_all (List.exists sat.Solver_intf.eval) cnf) then
raise Incorrect_model;
print "Sat (%f/%f)" t (Sys.time () -. t)
| Smt.Unsat us ->
let t = Sys.time () in
if !p_check then begin
let p = us.Solver_intf.get_proof () in
Smt.Proof.check p;
print_proof p;
if !p_unsat_core then
print_unsat_core (Smt.unsat_core p)
end;
print "Unsat (%f/%f)" t (Sys.time () -. t)
end
| Mcsat ->
Mcsat.assume cnf;
let res = Mcsat.solve () in
begin match res with
| Mcsat.Sat sat ->
let t = Sys.time () in
if !p_check then
if not (List.for_all (List.exists sat.Solver_intf.eval) cnf) then
raise Incorrect_model;
print "Sat (%f/%f)" t (Sys.time () -. t)
| Mcsat.Unsat us ->
let t = Sys.time () in
if !p_check then begin
let p = us.Solver_intf.get_proof () in
Mcsat.Proof.check p;
print_mcproof p;
if !p_unsat_core then
print_mc_unsat_core (Mcsat.unsat_core p)
end;
print "Unsat (%f/%f)" t (Sys.time () -. t)
end
*)

6
src/sat/sat.ml
View file

@ -5,9 +5,5 @@ Copyright 2014 Simon Cruanes
*)
module Make(Dummy : sig end) =
Msat.Solver.Make
(Msat.Expr.Atom)
(Msat.Solver.DummyTheory
(Msat.Expr.Atom))
(struct end)
Solver.Make(Expr.Atom)(Solver.DummyTheory(Expr.Atom))(struct end)

2
src/sat/sat.mli
View file

@ -4,8 +4,6 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
open Msat
module Make(Dummy : sig end) : Solver.S with type St.formula = Expr.Atom.t

2
src/smt/cc.ml
View file

@ -12,8 +12,6 @@
(* *)
(**************************************************************************)
open Msat
let max_split = 1000000
let cc_active = ref true

2
src/smt/mcsat.ml
View file

@ -4,8 +4,6 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
open Msat
module Fsmt = Expr
module Tsmt = struct

619
src/util/type.ml
View file

@ -1,610 +1,25 @@
(* Log&Module Init *)
(* ************************************************************************ *)
(** Typechecking of terms from Dolmen.Term.t
This module defines the requirements for typing expre'ssions from dolmen. *)
module Ast = Dolmen.Term
module Id = Dolmen.Id
module M = Map.Make(Id)
module H = Hashtbl.Make(Id)
module type S = sig
(* Types *)
(* ************************************************************************ *)
type atom
(** The type of atoms that will be fed to tha sovler. *)
(* The type of potentially expected result type for parsing an expression *)
type expect =
| Nothing
| Type
| Typed of Msat.Expr.ty
exception Typing_error of string * Dolmen.Term.t
(** Exception raised during typechecking. *)
(* The type returned after parsing an expression. *)
type res =
| Ttype
| Ty of Msat.Expr.ty
| Term of Msat.Expr.term
| Formula of Msat.Expr.Formula.t
val decl : Dolmen.Id.t -> Dolmen.Term.t -> unit
(** New declaration, i.e an identifier and its type. *)
val def : Dolmen.Id.t -> Dolmen.Term.t -> unit
(** New definition, i.e an identifier and the term it is equal to. *)
(* The local environments used for type-checking. *)
type env = {
(* local variables (mostly quantified variables) *)
type_vars : (Msat.Expr.ttype Msat.Expr.id) M.t;
term_vars : (Msat.Expr.ty Msat.Expr.id) M.t;
(* Bound variables (through let constructions) *)
term_lets : Msat.Expr.term M.t;
prop_lets : Msat.Expr.Formula.t M.t;
(* Typing options *)
expect : expect;
}
(* Exceptions *)
(* ************************************************************************ *)
(* Internal exception *)
exception Found of Ast.t
(* Exception for typing errors *)
exception Typing_error of string * Ast.t
(* Convenience functions *)
let _expected s t = raise (Typing_error (
Format.asprintf "Expected a %s" s, t))
let _bad_arity s n t = raise (Typing_error (
Format.asprintf "Bad arity for operator '%s' (expected %d arguments)" s n, t))
let _type_mismatch t ty ty' ast = raise (Typing_error (
Format.asprintf "Type Mismatch: '%a' has type %a, but an expression of type %a was expected"
Msat.Expr.Print.term t Msat.Expr.Print.ty ty Msat.Expr.Print.ty ty', ast))
let _fo_term s t = raise (Typing_error (
Format.asprintf "Let-bound variable '%a' is applied to terms" Id.print s, t))
(* Global Environment *)
(* ************************************************************************ *)
(* Global identifier table; stores declared types and aliases. *)
let global_env = H.create 42
let find_global name =
try H.find global_env name
with Not_found -> `Not_found
(* Symbol declarations *)
let decl_ty_cstr id c =
if H.mem global_env id then
Msat.Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition"
(fun k -> k Id.print id);
H.add global_env id (`Ty c);
Msat.Log.debugf 1 "New type constructor : %a" (fun k -> k Msat.Expr.Print.const_ttype c)
let decl_term id c =
if H.mem global_env id then
Msat.Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition"
(fun k -> k Id.print id);
H.add global_env id (`Term c);
Msat.Log.debugf 1 "New constant : %a" (fun k -> k Msat.Expr.Print.const_ty c)
(* Symbol definitions *)
let def_ty id args body =
if H.mem global_env id then
Msat.Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition"
(fun k -> k Id.print id);
H.add global_env id (`Ty_alias (args, body))
let def_term id ty_args args body =
if H.mem global_env id then
Msat.Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition"
(fun k -> k Id.print id);
H.add global_env id (`Term_alias (ty_args, args, body))
(* Local Environment *)
(* ************************************************************************ *)
(* Make a new empty environment *)
let empty_env ?(expect=Nothing) () = {
type_vars = M.empty;
term_vars = M.empty;
term_lets = M.empty;
prop_lets = M.empty;
expect;
}
(* Generate new fresh names for shadowed variables *)
let new_name pre =
let i = ref 0 in
(fun () -> incr i; pre ^ (string_of_int !i))
let new_ty_name = new_name "ty#"
let new_term_name = new_name "term#"
(* Add local variables to environment *)
let add_type_var env id v =
let v' =
if M.mem id env.type_vars then
Msat.Expr.Id.ttype (new_ty_name ())
else
v
in
Msat.Log.debugf 1 "New binding : %a -> %a"
(fun k -> k Id.print id Msat.Expr.Print.id_ttype v');
v', { env with type_vars = M.add id v' env.type_vars }
let add_type_vars env l =
let l', env' = List.fold_left (fun (l, acc) (id, v) ->
let v', acc' = add_type_var acc id v in
v' :: l, acc') ([], env) l in
List.rev l', env'
let add_term_var env id v =
let v' =
if M.mem id env.type_vars then
Msat.Expr.Id.ty (new_term_name ()) Msat.Expr.(v.id_type)
else
v
in
Msat.Log.debugf 1 "New binding : %a -> %a"
(fun k -> k Id.print id Msat.Expr.Print.id_ty v');
v', { env with term_vars = M.add id v' env.term_vars }
let find_var env name =
try `Ty (M.find name env.type_vars)
with Not_found ->
begin
try
`Term (M.find name env.term_vars)
with Not_found ->
`Not_found
end
(* Add local bound variables to env *)
let add_let_term env id t =
Msat.Log.debugf 1 "New let-binding : %s -> %a"
(fun k -> k id.Id.name Msat.Expr.Print.term t);
{ env with term_lets = M.add id t env.term_lets }
let add_let_prop env id t =
Msat.Log.debugf 1 "New let-binding : %s -> %a"
(fun k -> k id.Id.name Msat.Expr.Formula.print t);
{ env with prop_lets = M.add id t env.prop_lets }
let find_let env name =
try `Term (M.find name env.term_lets)
with Not_found ->
begin
try
`Prop (M.find name env.prop_lets)
with Not_found ->
`Not_found
end
let pp_expect fmt = function
| Nothing -> Format.fprintf fmt "<>"
| Type -> Format.fprintf fmt "<tType>"
| Typed ty -> Msat.Expr.Print.ty fmt ty
let pp_map pp fmt map =
M.iter (fun k v ->
Format.fprintf fmt "%s->%a;" k.Id.name pp v) map
(* Some helper functions *)
(* ************************************************************************ *)
let flat_map f l = List.flatten (List.map f l)
let take_drop n l =
let rec aux acc = function
| 0, _ | _, [] -> List.rev acc, []
| m, x :: r -> aux (x :: acc) (m - 1, r)
in
aux [] (n, l)
let diagonal l =
let rec single x acc = function
| [] -> acc
| y :: r -> single x ((x, y) :: acc) r
and aux acc = function
| [] -> acc
| x :: r -> aux (single x acc r) r
in
aux [] l
(* Wrappers for expression building *)
(* ************************************************************************ *)
let arity f =
List.length Msat.Expr.(f.id_type.fun_vars) +
List.length Msat.Expr.(f.id_type.fun_args)
let ty_apply env ast f args =
try
Msat.Expr.Ty.apply f args
with Msat.Expr.Bad_ty_arity _ ->
_bad_arity Msat.Expr.(f.id_name) (arity f) ast
let term_apply env ast f ty_args t_args =
try
Msat.Expr.Term.apply f ty_args t_args
with
| Msat.Expr.Bad_arity _ ->
_bad_arity Msat.Expr.(f.id_name) (arity f) ast
| Msat.Expr.Type_mismatch (t, ty, ty') ->
_type_mismatch t ty ty' ast
let ty_subst ast_term id args f_args body =
let aux s v ty = Msat.Expr.Subst.Id.bind v ty s in
match List.fold_left2 aux Msat.Expr.Subst.empty f_args args with
| subst ->
Msat.Expr.Ty.subst subst body
| exception Invalid_argument _ ->
_bad_arity id.Id.name (List.length f_args) ast_term
let term_subst ast_term id ty_args t_args f_ty_args f_t_args body =
let aux s v ty = Msat.Expr.Subst.Id.bind v ty s in
match List.fold_left2 aux Msat.Expr.Subst.empty f_ty_args ty_args with
| ty_subst ->
begin
let aux s v t = Msat.Expr.Subst.Id.bind v t s in
match List.fold_left2 aux Msat.Expr.Subst.empty f_t_args t_args with
| t_subst ->
Msat.Expr.Term.subst ty_subst t_subst body
| exception Invalid_argument _ ->
_bad_arity id.Id.name (List.length f_ty_args + List.length f_t_args) ast_term
end
| exception Invalid_argument _ ->
_bad_arity id.Id.name (List.length f_ty_args + List.length f_t_args) ast_term
let make_eq ast_term a b =
try
Msat.Expr.Formula.make_atom @@ Msat.Expr.Atom.eq a b
with Msat.Expr.Type_mismatch (t, ty, ty') ->
_type_mismatch t ty ty' ast_term
let make_pred ast_term p =
try
Msat.Expr.Formula.make_atom @@ Msat.Expr.Atom.pred p
with Msat.Expr.Type_mismatch (t, ty, ty') ->
_type_mismatch t ty ty' ast_term
let infer env s args =
match env.expect with
| Nothing -> `Nothing
| Type ->
let n = List.length args in
let res = Msat.Expr.Id.ty_fun s.Id.name n in
decl_ty_cstr s res;
`Ty res
| Typed ty ->
let n = List.length args in
let rec replicate acc n =
if n <= 0 then acc else replicate (Msat.Expr.Ty.base :: acc) (n - 1)
in
let res = Msat.Expr.Id.term_fun s.Id.name [] (replicate [] n) ty in
decl_term s res;
`Term res
(* Msat.Expression parsing *)
(* ************************************************************************ *)
let rec parse_expr (env : env) t =
match t with
(* Basic formulas *)
| { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.True }, []) }
| { Ast.term = Ast.Builtin Ast.True } ->
Formula Msat.Expr.Formula.f_true
| { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.False }, []) }
| { Ast.term = Ast.Builtin Ast.False } ->
Formula Msat.Expr.Formula.f_false
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And}, l) } ->
Formula (Msat.Expr.Formula.make_and (List.map (parse_formula env) l))
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or}, l) } ->
Formula (Msat.Expr.Formula.make_or (List.map (parse_formula env) l))
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor}, l) } as t ->
begin match l with
| [p; q] ->
let f = parse_formula env p in
let g = parse_formula env q in
Formula (Msat.Expr.Formula.make_not (Msat.Expr.Formula.make_equiv f g))
| _ -> _bad_arity "xor" 2 t
end
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Imply}, l) } as t ->
begin match l with
| [p; q] ->
let f = parse_formula env p in
let g = parse_formula env q in
Formula (Msat.Expr.Formula.make_imply f g)
| _ -> _bad_arity "=>" 2 t
end
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv}, l) } as t ->
begin match l with
| [p; q] ->
let f = parse_formula env p in
let g = parse_formula env q in
Formula (Msat.Expr.Formula.make_equiv f g)
| _ -> _bad_arity "<=>" 2 t
end
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not}, l) } as t ->
begin match l with
| [p] ->
Formula (Msat.Expr.Formula.make_not (parse_formula env p))
| _ -> _bad_arity "not" 1 t
end
(* (Dis)Equality *)
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, l) } as t ->
begin match l with
| [a; b] ->
Formula (
make_eq t
(parse_term env a)
(parse_term env b)
)
| _ -> _bad_arity "=" 2 t
end
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Distinct}, args) } as t ->
let l' = List.map (parse_term env) args in
let l'' = diagonal l' in
Formula (
Msat.Expr.Formula.make_and
(List.map (fun (a, b) ->
Msat.Expr.Formula.make_not
(make_eq t a b)) l'')
)
(* General case: application *)
| { Ast.term = Ast.Symbol s } as ast ->
parse_app env ast s []
| { Ast.term = Ast.App ({ Ast.term = Ast.Symbol s }, l) } as ast ->
parse_app env ast s l
(* Local bindings *)
| { Ast.term = Ast.Binder (Ast.Let, vars, f) } ->
parse_let env f vars
(* Other cases *)
| ast -> raise (Typing_error ("Couldn't parse the expression", ast))
and parse_var env = function
| { Ast.term = Ast.Colon ({ Ast.term = Ast.Symbol s }, e) } ->
begin match parse_expr env e with
| Ttype -> `Ty (s, Msat.Expr.Id.ttype s.Id.name)
| Ty ty -> `Term (s, Msat.Expr.Id.ty s.Id.name ty)
| _ -> _expected "type (or Ttype)" e
end
| { Ast.term = Ast.Symbol s } ->
begin match env.expect with
| Nothing -> assert false
| Type -> `Ty (s, Msat.Expr.Id.ttype s.Id.name)
| Typed ty -> `Term (s, Msat.Expr.Id.ty s.Id.name ty)
end
| t -> _expected "(typed) variable" t
and parse_quant_vars env l =
let ttype_vars, typed_vars, env' = List.fold_left (
fun (l1, l2, acc) v ->
match parse_var acc v with
| `Ty (id, v') ->
let v'', acc' = add_type_var acc id v' in
(v'' :: l1, l2, acc')
| `Term (id, v') ->
let v'', acc' = add_term_var acc id v' in
(l1, v'' :: l2, acc')
) ([], [], env) l in
List.rev ttype_vars, List.rev typed_vars, env'
and parse_let env f = function
| [] -> parse_expr env f
| x :: r ->
begin match x with
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, [
{ Ast.term = Ast.Symbol s }; e]) } ->
let t = parse_term env e in
let env' = add_let_term env s t in
parse_let env' f r
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv}, [
{ Ast.term = Ast.Symbol s }; e]) } ->
let t = parse_formula env e in
let env' = add_let_prop env s t in
parse_let env' f r
| { Ast.term = Ast.Colon ({ Ast.term = Ast.Symbol s }, e) } ->
begin match parse_expr env e with
| Term t ->
let env' = add_let_term env s t in
parse_let env' f r
| Formula t ->
let env' = add_let_prop env s t in
parse_let env' f r
| _ -> _expected "term of formula" e
end
| t -> _expected "let-binding" t
end
and parse_app env ast s args =
match find_let env s with
| `Term t ->
if args = [] then Term t
else _fo_term s ast
| `Prop p ->
if args = [] then Formula p
else _fo_term s ast
| `Not_found ->
begin match find_var env s with
| `Ty f ->
if args = [] then Ty (Msat.Expr.Ty.of_id f)
else _fo_term s ast
| `Term f ->
if args = [] then Term (Msat.Expr.Term.of_id f)
else _fo_term s ast
| `Not_found ->
begin match find_global s with
| `Ty f ->
parse_app_ty env ast f args
| `Term f ->
parse_app_term env ast f args
| `Ty_alias (f_args, body) ->
parse_app_subst_ty env ast s args f_args body
| `Term_alias (f_ty_args, f_t_args, body) ->
parse_app_subst_term env ast s args f_ty_args f_t_args body
| `Not_found ->
begin match infer env s args with
| `Ty f -> parse_app_ty env ast f args
| `Term f -> parse_app_term env ast f args
| `Nothing ->
raise (Typing_error (
Format.asprintf "Scoping error: '%a' not found" Id.print s, ast))
end
end
end
and parse_app_ty env ast f args =
let l = List.map (parse_ty env) args in
Ty (ty_apply env ast f l)
and parse_app_term env ast f args =
let n = List.length Msat.Expr.(f.id_type.fun_vars) in
let ty_l, t_l = take_drop n args in
let ty_args = List.map (parse_ty env) ty_l in
let t_args = List.map (parse_term env) t_l in
Term (term_apply env ast f ty_args t_args)
and parse_app_subst_ty env ast id args f_args body =
let l = List.map (parse_ty env) args in
Ty (ty_subst ast id l f_args body)
and parse_app_subst_term env ast id args f_ty_args f_t_args body =
let n = List.length f_ty_args in
let ty_l, t_l = take_drop n args in
let ty_args = List.map (parse_ty env) ty_l in
let t_args = List.map (parse_term env) t_l in
Term (term_subst ast id ty_args t_args f_ty_args f_t_args body)
and parse_ty env ast =
match parse_expr { env with expect = Type } ast with
| Ty ty -> ty
| _ -> _expected "type" ast
and parse_term env ast =
match parse_expr { env with expect = Typed Msat.Expr.Ty.base } ast with
| Term t -> t
| _ -> _expected "term" ast
and parse_formula env ast =
match parse_expr { env with expect = Typed Msat.Expr.Ty.prop } ast with
| Term t when Msat.Expr.(Ty.equal Ty.prop t.t_type) ->
make_pred ast t
| Formula p -> p
| _ -> _expected "formula" ast
let parse_ttype_var env t =
match parse_var env t with
| `Ty (id, v) -> (id, v)
| `Term _ -> _expected "type variable" t
let rec parse_sig_quant env = function
| { Ast.term = Ast.Binder (Ast.Pi, vars, t) } ->
let ttype_vars = List.map (parse_ttype_var env) vars in
let ttype_vars', env' = add_type_vars env ttype_vars in
let l = List.combine vars ttype_vars' in
parse_sig_arrow l [] env' t
| t ->
parse_sig_arrow [] [] env t
and parse_sig_arrow ttype_vars (ty_args: (Ast.t * res) list) env = function
| { Ast.term = Ast.Binder (Ast.Arrow, args, ret) } ->
let t_args = parse_sig_args env args in
parse_sig_arrow ttype_vars (ty_args @ t_args) env ret
| t ->
begin match parse_expr env t with
| Ttype ->
begin match ttype_vars with
| (h, _) :: _ ->
raise (Typing_error (
"Type constructor signatures cannot have quantified type variables", h))
| [] ->
let aux n = function
| (_, Ttype) -> n + 1
| (ast, _) -> raise (Found ast)
in
begin
match List.fold_left aux 0 ty_args with
| n -> `Ty_cstr n
| exception Found err ->
raise (Typing_error (
Format.asprintf
"Type constructor signatures cannot have non-ttype arguments,", err))
end
end
| Ty ret ->
let aux acc = function
| (_, Ty t) -> t :: acc
| (ast, _) -> raise (Found ast)
in
begin
match List.fold_left aux [] ty_args with
| exception Found err -> _expected "type" err
| l -> `Fun_ty (List.map snd ttype_vars, List.rev l, ret)
end
| _ -> _expected "Ttype of type" t
end
and parse_sig_args env l =
flat_map (parse_sig_arg env) l
and parse_sig_arg env = function
| { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.Product}, l) } ->
List.map (fun x -> x, parse_expr env x) l
| t ->
[t, parse_expr env t]
let parse_sig = parse_sig_quant
let rec parse_fun ty_args t_args env = function
| { Ast.term = Ast.Binder (Ast.Fun, l, ret) } ->
let ty_args', t_args', env' = parse_quant_vars env l in
parse_fun (ty_args @ ty_args') (t_args @ t_args') env' ret
| ast ->
begin match parse_expr env ast with
| Ttype -> raise (Typing_error ("Cannot redefine Ttype", ast))
| Ty body ->
if t_args = [] then `Ty (ty_args, body)
else _expected "term" ast
| Term body -> `Term (ty_args, t_args, body)
| Formula _ -> _expected "type or term" ast
end
(* High-level parsing functions *)
(* ************************************************************************ *)
let new_decl id t =
let env = empty_env () in
Msat.Log.debugf 5 "Typing declaration: %s : %a"
(fun k -> k id.Id.name Ast.print t);
begin match parse_sig env t with
| `Ty_cstr n -> decl_ty_cstr id (Msat.Expr.Id.ty_fun id.Id.name n)
| `Fun_ty (vars, args, ret) ->
decl_term id (Msat.Expr.Id.term_fun id.Id.name vars args ret)
end
let new_def id t =
let env = empty_env () in
Msat.Log.debugf 5 "Typing definition: %s = %a"
(fun k -> k id.Id.name Ast.print t);
begin match parse_fun [] [] env t with
| `Ty (ty_args, body) -> def_ty id ty_args body
| `Term (ty_args, t_args, body) -> def_term id ty_args t_args body
end
let new_formula t =
let env = empty_env () in
Msat.Log.debugf 5 "Typing top-level formula: %a" (fun k -> k Ast.print t);
let res = parse_formula env t in
res
val consequent : Dolmen.Term.t -> atom list list
val antecedent : Dolmen.Term.t -> atom list list
(** Parse a formula, and return a cnf ready to be given to the solver.
Consequent is for hypotheses (left of the sequent), while antecedent
is for goals (i.e formulas on the right of a sequent). *)
end

15
src/util/type.mli
View file

@ -1,15 +0,0 @@
(** Typechecking of terms from Dolmen.Term.t
This module provides functions to parse terms from the untyped syntax tree
defined in Dolmen, and generate formulas as defined in the Expr module. *)
exception Typing_error of string * Dolmen.Term.t
(** {2 High-level functions} *)
val new_decl : Dolmen.Id.t -> Dolmen.Term.t -> unit
val new_def : Dolmen.Id.t -> Dolmen.Term.t -> unit
val new_formula : Dolmen.Term.t -> Msat.Expr.Formula.t

615
src/util/type_smt.ml Normal file
View file

@ -0,0 +1,615 @@
(* Log&Module Init *)
(* ************************************************************************ *)
module Ast = Dolmen.Term
module Id = Dolmen.Id
module M = Map.Make(Id)
module H = Hashtbl.Make(Id)
(* Types *)
(* ************************************************************************ *)
(* The type of potentially expected result type for parsing an expression *)
type expect =
| Nothing
| Type
| Typed of Expr.ty
(* The type returned after parsing an expression. *)
type res =
| Ttype
| Ty of Expr.ty
| Term of Expr.term
| Formula of Expr.Formula.t
(* The local environments used for type-checking. *)
type env = {
(* local variables (mostly quantified variables) *)
type_vars : (Expr.ttype Expr.id) M.t;
term_vars : (Expr.ty Expr.id) M.t;
(* Bound variables (through let constructions) *)
term_lets : Expr.term M.t;
prop_lets : Expr.Formula.t M.t;
(* Typing options *)
expect : expect;
}
(* Exceptions *)
(* ************************************************************************ *)
(* Internal exception *)
exception Found of Ast.t
(* Exception for typing errors *)
exception Typing_error of string * Ast.t
(* Convenience functions *)
let _expected s t = raise (Typing_error (
Format.asprintf "Expected a %s" s, t))
let _bad_arity s n t = raise (Typing_error (
Format.asprintf "Bad arity for operator '%s' (expected %d arguments)" s n, t))
let _type_mismatch t ty ty' ast = raise (Typing_error (
Format.asprintf "Type Mismatch: '%a' has type %a, but an expression of type %a was expected"
Expr.Print.term t Expr.Print.ty ty Expr.Print.ty ty', ast))
let _fo_term s t = raise (Typing_error (
Format.asprintf "Let-bound variable '%a' is applied to terms" Id.print s, t))
(* Global Environment *)
(* ************************************************************************ *)
(* Global identifier table; stores declared types and aliases. *)
let global_env = H.create 42
let find_global name =
try H.find global_env name
with Not_found -> `Not_found
(* Symbol declarations *)
let decl_ty_cstr id c =
if H.mem global_env id then
Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition"
(fun k -> k Id.print id);
H.add global_env id (`Ty c);
Log.debugf 1 "New type constructor : %a" (fun k -> k Expr.Print.const_ttype c)
let decl_term id c =
if H.mem global_env id then
Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition"
(fun k -> k Id.print id);
H.add global_env id (`Term c);
Log.debugf 1 "New constant : %a" (fun k -> k Expr.Print.const_ty c)
(* Symbol definitions *)
let def_ty id args body =
if H.mem global_env id then
Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition"
(fun k -> k Id.print id);
H.add global_env id (`Ty_alias (args, body))
let def_term id ty_args args body =
if H.mem global_env id then
Log.debugf 0 "Symbol '%a' has already been defined, overwriting previous definition"
(fun k -> k Id.print id);
H.add global_env id (`Term_alias (ty_args, args, body))
(* Local Environment *)
(* ************************************************************************ *)
(* Make a new empty environment *)
let empty_env ?(expect=Nothing) () = {
type_vars = M.empty;
term_vars = M.empty;
term_lets = M.empty;
prop_lets = M.empty;
expect;
}
(* Generate new fresh names for shadowed variables *)
let new_name pre =
let i = ref 0 in
(fun () -> incr i; pre ^ (string_of_int !i))
let new_ty_name = new_name "ty#"
let new_term_name = new_name "term#"
(* Add local variables to environment *)
let add_type_var env id v =
let v' =
if M.mem id env.type_vars then
Expr.Id.ttype (new_ty_name ())
else
v
in
Log.debugf 1 "New binding : %a -> %a"
(fun k -> k Id.print id Expr.Print.id_ttype v');
v', { env with type_vars = M.add id v' env.type_vars }
let add_type_vars env l =
let l', env' = List.fold_left (fun (l, acc) (id, v) ->
let v', acc' = add_type_var acc id v in
v' :: l, acc') ([], env) l in
List.rev l', env'
let add_term_var env id v =
let v' =
if M.mem id env.type_vars then
Expr.Id.ty (new_term_name ()) Expr.(v.id_type)
else
v
in
Log.debugf 1 "New binding : %a -> %a"
(fun k -> k Id.print id Expr.Print.id_ty v');
v', { env with term_vars = M.add id v' env.term_vars }
let find_var env name =
try `Ty (M.find name env.type_vars)
with Not_found ->
begin
try
`Term (M.find name env.term_vars)
with Not_found ->
`Not_found
end
(* Add local bound variables to env *)
let add_let_term env id t =
Log.debugf 1 "New let-binding : %s -> %a"
(fun k -> k id.Id.name Expr.Print.term t);
{ env with term_lets = M.add id t env.term_lets }
let add_let_prop env id t =
Log.debugf 1 "New let-binding : %s -> %a"
(fun k -> k id.Id.name Expr.Formula.print t);
{ env with prop_lets = M.add id t env.prop_lets }
let find_let env name =
try `Term (M.find name env.term_lets)
with Not_found ->
begin
try
`Prop (M.find name env.prop_lets)
with Not_found ->
`Not_found
end
let pp_expect fmt = function
| Nothing -> Format.fprintf fmt "<>"
| Type -> Format.fprintf fmt "<tType>"
| Typed ty -> Expr.Print.ty fmt ty
let pp_map pp fmt map =
M.iter (fun k v ->
Format.fprintf fmt "%s->%a;" k.Id.name pp v) map
(* Some helper functions *)
(* ************************************************************************ *)
let flat_map f l = List.flatten (List.map f l)
let take_drop n l =
let rec aux acc = function
| 0, _ | _, [] -> List.rev acc, []
| m, x :: r -> aux (x :: acc) (m - 1, r)
in
aux [] (n, l)
let diagonal l =
let rec single x acc = function
| [] -> acc
| y :: r -> single x ((x, y) :: acc) r
and aux acc = function
| [] -> acc
| x :: r -> aux (single x acc r) r
in
aux [] l
(* Wrappers for expression building *)
(* ************************************************************************ *)
let arity f =
List.length Expr.(f.id_type.fun_vars) +
List.length Expr.(f.id_type.fun_args)
let ty_apply env ast f args =
try
Expr.Ty.apply f args
with Expr.Bad_ty_arity _ ->
_bad_arity Expr.(f.id_name) (arity f) ast
let term_apply env ast f ty_args t_args =
try
Expr.Term.apply f ty_args t_args
with
| Expr.Bad_arity _ ->
_bad_arity Expr.(f.id_name) (arity f) ast
| Expr.Type_mismatch (t, ty, ty') ->
_type_mismatch t ty ty' ast
let ty_subst ast_term id args f_args body =
let aux s v ty = Expr.Subst.Id.bind v ty s in
match List.fold_left2 aux Expr.Subst.empty f_args args with
| subst ->
Expr.Ty.subst subst body
| exception Invalid_argument _ ->
_bad_arity id.Id.name (List.length f_args) ast_term
let term_subst ast_term id ty_args t_args f_ty_args f_t_args body =
let aux s v ty = Expr.Subst.Id.bind v ty s in
match List.fold_left2 aux Expr.Subst.empty f_ty_args ty_args with
| ty_subst ->
begin
let aux s v t = Expr.Subst.Id.bind v t s in
match List.fold_left2 aux Expr.Subst.empty f_t_args t_args with
| t_subst ->
Expr.Term.subst ty_subst t_subst body
| exception Invalid_argument _ ->
_bad_arity id.Id.name (List.length f_ty_args + List.length f_t_args) ast_term
end
| exception Invalid_argument _ ->
_bad_arity id.Id.name (List.length f_ty_args + List.length f_t_args) ast_term
let make_eq ast_term a b =
try
Expr.Formula.make_atom @@ Expr.Atom.eq a b
with Expr.Type_mismatch (t, ty, ty') ->
_type_mismatch t ty ty' ast_term
let make_pred ast_term p =
try
Expr.Formula.make_atom @@ Expr.Atom.pred p
with Expr.Type_mismatch (t, ty, ty') ->
_type_mismatch t ty ty' ast_term
let infer env s args =
match env.expect with
| Nothing -> `Nothing
| Type ->
let n = List.length args in
let res = Expr.Id.ty_fun s.Id.name n in
decl_ty_cstr s res;
`Ty res
| Typed ty ->
let n = List.length args in
let rec replicate acc n =
if n <= 0 then acc else replicate (Expr.Ty.base :: acc) (n - 1)
in
let res = Expr.Id.term_fun s.Id.name [] (replicate [] n) ty in
decl_term s res;
`Term res
(* Expression parsing *)
(* ************************************************************************ *)
let rec parse_expr (env : env) t =
match t with
(* Basic formulas *)
| { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.True }, []) }
| { Ast.term = Ast.Builtin Ast.True } ->
Formula Expr.Formula.f_true
| { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.False }, []) }
| { Ast.term = Ast.Builtin Ast.False } ->
Formula Expr.Formula.f_false
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And}, l) } ->
Formula (Expr.Formula.make_and (List.map (parse_formula env) l))
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or}, l) } ->
Formula (Expr.Formula.make_or (List.map (parse_formula env) l))
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor}, l) } as t ->
begin match l with
| [p; q] ->
let f = parse_formula env p in
let g = parse_formula env q in
Formula (Expr.Formula.make_not (Expr.Formula.make_equiv f g))
| _ -> _bad_arity "xor" 2 t
end
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Imply}, l) } as t ->
begin match l with
| [p; q] ->
let f = parse_formula env p in
let g = parse_formula env q in
Formula (Expr.Formula.make_imply f g)
| _ -> _bad_arity "=>" 2 t
end
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv}, l) } as t ->
begin match l with
| [p; q] ->
let f = parse_formula env p in
let g = parse_formula env q in
Formula (Expr.Formula.make_equiv f g)
| _ -> _bad_arity "<=>" 2 t
end
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not}, l) } as t ->
begin match l with
| [p] ->
Formula (Expr.Formula.make_not (parse_formula env p))
| _ -> _bad_arity "not" 1 t
end
(* (Dis)Equality *)
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, l) } as t ->
begin match l with
| [a; b] ->
Formula (
make_eq t
(parse_term env a)
(parse_term env b)
)
| _ -> _bad_arity "=" 2 t
end
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Distinct}, args) } as t ->
let l' = List.map (parse_term env) args in
let l'' = diagonal l' in
Formula (
Expr.Formula.make_and
(List.map (fun (a, b) ->
Expr.Formula.make_not
(make_eq t a b)) l'')
)
(* General case: application *)
| { Ast.term = Ast.Symbol s } as ast ->
parse_app env ast s []
| { Ast.term = Ast.App ({ Ast.term = Ast.Symbol s }, l) } as ast ->
parse_app env ast s l
(* Local bindings *)
| { Ast.term = Ast.Binder (Ast.Let, vars, f) } ->
parse_let env f vars
(* Other cases *)
| ast -> raise (Typing_error ("Couldn't parse the expression", ast))
and parse_var env = function
| { Ast.term = Ast.Colon ({ Ast.term = Ast.Symbol s }, e) } ->
begin match parse_expr env e with
| Ttype -> `Ty (s, Expr.Id.ttype s.Id.name)
| Ty ty -> `Term (s, Expr.Id.ty s.Id.name ty)
| _ -> _expected "type (or Ttype)" e
end
| { Ast.term = Ast.Symbol s } ->
begin match env.expect with
| Nothing -> assert false
| Type -> `Ty (s, Expr.Id.ttype s.Id.name)
| Typed ty -> `Term (s, Expr.Id.ty s.Id.name ty)
end
| t -> _expected "(typed) variable" t
and parse_quant_vars env l =
let ttype_vars, typed_vars, env' = List.fold_left (
fun (l1, l2, acc) v ->
match parse_var acc v with
| `Ty (id, v') ->
let v'', acc' = add_type_var acc id v' in
(v'' :: l1, l2, acc')
| `Term (id, v') ->
let v'', acc' = add_term_var acc id v' in
(l1, v'' :: l2, acc')
) ([], [], env) l in
List.rev ttype_vars, List.rev typed_vars, env'
and parse_let env f = function
| [] -> parse_expr env f
| x :: r ->
begin match x with
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, [
{ Ast.term = Ast.Symbol s }; e]) } ->
let t = parse_term env e in
let env' = add_let_term env s t in
parse_let env' f r
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv}, [
{ Ast.term = Ast.Symbol s }; e]) } ->
let t = parse_formula env e in
let env' = add_let_prop env s t in
parse_let env' f r
| { Ast.term = Ast.Colon ({ Ast.term = Ast.Symbol s }, e) } ->
begin match parse_expr env e with
| Term t ->
let env' = add_let_term env s t in
parse_let env' f r
| Formula t ->
let env' = add_let_prop env s t in
parse_let env' f r
| _ -> _expected "term of formula" e
end
| t -> _expected "let-binding" t
end
and parse_app env ast s args =
match find_let env s with
| `Term t ->
if args = [] then Term t
else _fo_term s ast
| `Prop p ->
if args = [] then Formula p
else _fo_term s ast
| `Not_found ->
begin match find_var env s with
| `Ty f ->
if args = [] then Ty (Expr.Ty.of_id f)
else _fo_term s ast
| `Term f ->
if args = [] then Term (Expr.Term.of_id f)
else _fo_term s ast
| `Not_found ->
begin match find_global s with
| `Ty f ->
parse_app_ty env ast f args
| `Term f ->
parse_app_term env ast f args
| `Ty_alias (f_args, body) ->
parse_app_subst_ty env ast s args f_args body
| `Term_alias (f_ty_args, f_t_args, body) ->
parse_app_subst_term env ast s args f_ty_args f_t_args body
| `Not_found ->
begin match infer env s args with
| `Ty f -> parse_app_ty env ast f args
| `Term f -> parse_app_term env ast f args
| `Nothing ->
raise (Typing_error (
Format.asprintf "Scoping error: '%a' not found" Id.print s, ast))
end
end
end
and parse_app_ty env ast f args =
let l = List.map (parse_ty env) args in
Ty (ty_apply env ast f l)
and parse_app_term env ast f args =
let n = List.length Expr.(f.id_type.fun_vars) in
let ty_l, t_l = take_drop n args in
let ty_args = List.map (parse_ty env) ty_l in
let t_args = List.map (parse_term env) t_l in
Term (term_apply env ast f ty_args t_args)
and parse_app_subst_ty env ast id args f_args body =
let l = List.map (parse_ty env) args in
Ty (ty_subst ast id l f_args body)
and parse_app_subst_term env ast id args f_ty_args f_t_args body =
let n = List.length f_ty_args in
let ty_l, t_l = take_drop n args in
let ty_args = List.map (parse_ty env) ty_l in
let t_args = List.map (parse_term env) t_l in
Term (term_subst ast id ty_args t_args f_ty_args f_t_args body)
and parse_ty env ast =
match parse_expr { env with expect = Type } ast with
| Ty ty -> ty
| _ -> _expected "type" ast
and parse_term env ast =
match parse_expr { env with expect = Typed Expr.Ty.base } ast with
| Term t -> t
| _ -> _expected "term" ast
and parse_formula env ast =
match parse_expr { env with expect = Typed Expr.Ty.prop } ast with
| Term t when Expr.(Ty.equal Ty.prop t.t_type) ->
make_pred ast t
| Formula p -> p
| _ -> _expected "formula" ast
let parse_ttype_var env t =
match parse_var env t with
| `Ty (id, v) -> (id, v)
| `Term _ -> _expected "type variable" t
let rec parse_sig_quant env = function
| { Ast.term = Ast.Binder (Ast.Pi, vars, t) } ->
let ttype_vars = List.map (parse_ttype_var env) vars in
let ttype_vars', env' = add_type_vars env ttype_vars in
let l = List.combine vars ttype_vars' in
parse_sig_arrow l [] env' t
| t ->
parse_sig_arrow [] [] env t
and parse_sig_arrow ttype_vars (ty_args: (Ast.t * res) list) env = function
| { Ast.term = Ast.Binder (Ast.Arrow, args, ret) } ->
let t_args = parse_sig_args env args in
parse_sig_arrow ttype_vars (ty_args @ t_args) env ret
| t ->
begin match parse_expr env t with
| Ttype ->
begin match ttype_vars with
| (h, _) :: _ ->
raise (Typing_error (
"Type constructor signatures cannot have quantified type variables", h))
| [] ->
let aux n = function
| (_, Ttype) -> n + 1
| (ast, _) -> raise (Found ast)
in
begin
match List.fold_left aux 0 ty_args with
| n -> `Ty_cstr n
| exception Found err ->
raise (Typing_error (
Format.asprintf
"Type constructor signatures cannot have non-ttype arguments,", err))
end
end
| Ty ret ->
let aux acc = function
| (_, Ty t) -> t :: acc
| (ast, _) -> raise (Found ast)
in
begin
match List.fold_left aux [] ty_args with
| exception Found err -> _expected "type" err
| l -> `Fun_ty (List.map snd ttype_vars, List.rev l, ret)
end
| _ -> _expected "Ttype of type" t
end
and parse_sig_args env l =
flat_map (parse_sig_arg env) l
and parse_sig_arg env = function
| { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.Product}, l) } ->
List.map (fun x -> x, parse_expr env x) l
| t ->
[t, parse_expr env t]
let parse_sig = parse_sig_quant
let rec parse_fun ty_args t_args env = function
| { Ast.term = Ast.Binder (Ast.Fun, l, ret) } ->
let ty_args', t_args', env' = parse_quant_vars env l in
parse_fun (ty_args @ ty_args') (t_args @ t_args') env' ret
| ast ->
begin match parse_expr env ast with
| Ttype -> raise (Typing_error ("Cannot redefine Ttype", ast))
| Ty body ->
if t_args = [] then `Ty (ty_args, body)
else _expected "term" ast
| Term body -> `Term (ty_args, t_args, body)
| Formula _ -> _expected "type or term" ast
end
(* High-level parsing functions *)
(* ************************************************************************ *)
let decl id t =
let env = empty_env () in
Log.debugf 5 "Typing declaration: %s : %a"
(fun k -> k id.Id.name Ast.print t);
begin match parse_sig env t with
| `Ty_cstr n -> decl_ty_cstr id (Expr.Id.ty_fun id.Id.name n)
| `Fun_ty (vars, args, ret) ->
decl_term id (Expr.Id.term_fun id.Id.name vars args ret)
end
let def id t =
let env = empty_env () in
Log.debugf 5 "Typing definition: %s = %a"
(fun k -> k id.Id.name Ast.print t);
begin match parse_fun [] [] env t with
| `Ty (ty_args, body) -> def_ty id ty_args body
| `Term (ty_args, t_args, body) -> def_term id ty_args t_args body
end
let formula t =
let env = empty_env () in
Log.debugf 5 "Typing top-level formula: %a" (fun k -> k Ast.print t);
parse_formula env t
let consequent t =
Expr.Formula.make_cnf (formula t)
let antecedent t =
Expr.Formula.make_cnf (Expr.Formula.make_not (formula t))

7
src/util/type_smt.mli Normal file
View file

@ -0,0 +1,7 @@
(** Typechecking of terms from Dolmen.Term.t
This module provides functions to parse terms from the untyped syntax tree
defined in Dolmen, and generate formulas as defined in the Expr module. *)
include Type.S with type atom = Expr.atom