Something went wrong. Try again.
forked from gbury/dolmen
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437
(* Merging builtin parser functions *)(* ************************************************************************ *)
let noop _ _ = `Not_found
let rec merge l env s = match l with | [] -> `Not_found | f :: r -> begin match f env s with | `Not_found -> merge r env s | ret -> ret end
(* Smtlib ID splitting *)(* ************************************************************************ *)
type 'ret indexed = [ | `Not_indexed | `Unary of (string -> 'ret) | `Binary of (string -> string -> 'ret) | `Ternary of (string -> string -> string -> 'ret) | `Nary of int * (string list -> 'ret)]
let parse_indexed h r f ~err ~k = let r_l = List.length r in match f h with | `Not_indexed -> k () | `Unary f -> begin match r with | [x] -> f x | _ -> err h 1 r_l end | `Binary f -> begin match r with | [x; y] -> f x y | _ -> err h 2 r_l end | `Ternary f -> begin match r with | [x; y; z] -> f x y z | _ -> err h 3 r_l end | `Nary (n, f') -> if n = r_l then f' r else err h n r_l
let bad_ty_index_arity (type env ty) (module Type: Tff_intf.S with type env = env and type Ty.t = ty) env s n r_l = `Ty ( (), fun ast _args -> Type._error env (Ast ast) (Type.Bad_index_arity (s, Exact n, r_l)) )
let bad_term_index_arity (type env term) (module Type: Tff_intf.S with type env = env and type T.t = term) env s n r_l = `Term (`Total, fun ast _args -> Type._error env (Ast ast) (Type.Bad_index_arity (s, Exact n, r_l)) )
(* Low level helpers *)(* ************************************************************************ *)
type ('env, 'args, 'ret) helper = (module Tff_intf.S with type env = 'env) -> 'env -> Intf.symbol -> (Dolmen.Std.Term.t -> 'args -> 'ret) -> (Dolmen.Std.Term.t -> Dolmen.Std.Term.t list -> 'ret)
let make_op0 (type env) (module Type: Tff_intf.S with type env = env) env op ret = fun ast args -> match args with | [] -> ret ast () | _ -> Type._error env (Ast ast) (Type.Bad_op_arity (op, Exact 0, List.length args))
let make_op1 (type env) (module Type: Tff_intf.S with type env = env) env op ret = fun ast args -> match args with | [t1] -> ret ast t1 | _ -> Type._error env (Ast ast) (Type.Bad_op_arity (op, Exact 1, List.length args))
let make_op2 (type env) (module Type: Tff_intf.S with type env = env) env op ret = fun ast args -> match args with | [t1; t2] -> ret ast (t1, t2) | _ -> Type._error env (Ast ast) (Type.Bad_op_arity (op, Exact 2, List.length args))
let make_op3 (type env) (module Type: Tff_intf.S with type env = env) env op ret = fun ast args -> match args with | [t1; t2; t3] -> ret ast (t1, t2, t3) | _ -> Type._error env (Ast ast) (Type.Bad_op_arity (op, Exact 3, List.length args))
let make_op4 (type env) (module Type: Tff_intf.S with type env = env) env op ret = fun ast args -> match args with | [t1; t2; t3; t4] -> ret ast (t1, t2, t3, t4) | _ -> Type._error env (Ast ast) (Type.Bad_op_arity (op, Exact 4, List.length args))
let make_opn n (type env) (module Type: Tff_intf.S with type env = env) env op ret = fun ast args -> let l = List.length args in if l = n then ret ast args else begin Type._error env (Ast ast) (Type.Bad_op_arity (op, Exact n, l)) end
let make_assoc (type env) (module Type: Tff_intf.S with type env = env) env op ret = fun ast args -> match args with | [] | [_] -> Type._error env (Ast ast) (Type.Bad_op_arity (op, At_least 2, List.length args)) | _ -> ret ast args
let make_assoc' (type env) (module Type: Tff_intf.S with type env = env) env op ret = fun ast f args -> match args with | [] -> Type._error env (Ast ast) (Type.Bad_op_arity (op, At_least 2, List.length args)) | _ -> ret ast f args
let fold_left_assoc mk = function | h :: r -> List.fold_left mk h r | _ -> raise (Invalid_argument "Base.fold_left_assoc")
let rec fold_right_assoc mk = function | [x] -> x | h :: r -> mk h (fold_right_assoc mk r) | _ -> raise (Invalid_argument "Base.fold_right_assoc")
let make_chain = make_assoc
let map_chain (type t) (module Type: Tff_intf.S with type T.t = t) mk args = let rec aux mk = function | [] -> assert false | [_] -> [] | x :: ((y :: _) as r) -> mk x y :: aux mk r in match aux mk args with | [] -> assert false | [x] -> x | l -> fold_left_assoc (fun a b -> Type.T._and [a; b]) l
(* High level helpers *)(* ************************************************************************ *)
(* Nullary applications *)
let app0 (type env) (module Type : Tff_intf.S with type env = env) ?(check=(fun _ -> ())) env symbol ret = make_op0 (module Type) env symbol (fun ast () -> check ast; ret)
let app0_ast (type env) (module Type : Tff_intf.S with type env = env) ?(check=(fun _ -> ())) env symbol mk = make_op0 (module Type) env symbol (fun ast () -> check ast; mk ast)
(* Unary applications *)
let ty_app1 (type env) (type ty) (module Type : Tff_intf.S with type env = env and type Ty.t = ty) ?(check=(fun _ _ -> ())) env symbol mk = make_op1 (module Type) env symbol (fun ast t -> check ast t; mk (Type.parse_ty env t))
let ty_app1_ast (type env) (type ty) (module Type : Tff_intf.S with type env = env and type Ty.t = ty) ?(check=(fun _ _ -> ())) env symbol mk = make_op1 (module Type) env symbol (fun ast t -> check ast t; mk ast (Type.parse_ty env t))
let term_app1 (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) ?(check=(fun _ _ -> ())) env symbol mk = make_op1 (module Type) env symbol (fun ast t -> check ast t; mk (Type.parse_term env t))
let term_app1_ast (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) ?(check=(fun _ _ -> ())) env symbol mk = make_op1 (module Type) env symbol (fun ast t -> check ast t; mk ast (Type.parse_term env t))
(* Binary applications *)
let ty_app2 (type env) (type ty) (module Type : Tff_intf.S with type env = env and type Ty.t = ty) ?(check=(fun _ _ _ -> ())) env symbol mk = make_op2 (module Type) env symbol (fun ast (a, b) -> check ast a b; mk (Type.parse_ty env a) (Type.parse_ty env b))
let ty_app2_ast (type env) (type ty) (module Type : Tff_intf.S with type env = env and type Ty.t = ty) ?(check=(fun _ _ _ -> ())) env symbol mk = make_op2 (module Type) env symbol (fun ast (a, b) -> check ast a b; mk ast (Type.parse_ty env a) (Type.parse_ty env b))
let term_app2 (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) ?(check=(fun _ _ _ -> ())) env symbol mk = make_op2 (module Type) env symbol (fun ast (a, b) -> check ast a b; mk (Type.parse_term env a) (Type.parse_term env b))
let term_app2_ast (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) ?(check=(fun _ _ _ -> ())) env symbol mk = make_op2 (module Type) env symbol (fun ast (a, b) -> check ast a b; mk ast (Type.parse_term env a) (Type.parse_term env b))
(* Ternary applications *)
let ty_app3 (type env) (type ty) (module Type : Tff_intf.S with type env = env and type Ty.t = ty) ?(check=(fun _ _ _ _ -> ())) env symbol mk = make_op3 (module Type) env symbol (fun ast (a, b, c) -> check ast a b c; mk (Type.parse_ty env a) (Type.parse_ty env b) (Type.parse_ty env c))
let ty_app3_ast (type env) (type ty) (module Type : Tff_intf.S with type env = env and type Ty.t = ty) ?(check=(fun _ _ _ _ -> ())) env symbol mk = make_op3 (module Type) env symbol (fun ast (a, b, c) -> check ast a b c; mk ast (Type.parse_ty env a) (Type.parse_ty env b) (Type.parse_ty env c))
let term_app3 (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) ?(check=(fun _ _ _ _ -> ())) env symbol mk = make_op3 (module Type) env symbol (fun ast (a, b, c) -> check ast a b c; mk (Type.parse_term env a) (Type.parse_term env b) (Type.parse_term env c))
let term_app3_ast (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) ?(check=(fun _ _ _ _ -> ())) env symbol mk = make_op3 (module Type) env symbol (fun ast (a, b, c) -> check ast a b c; mk ast (Type.parse_term env a) (Type.parse_term env b) (Type.parse_term env c))
(* Quaternary applications *)
let ty_app4 (type env) (type ty) (module Type : Tff_intf.S with type env = env and type Ty.t = ty) ?(check=(fun _ _ _ _ _ -> ())) env symbol mk = make_op4 (module Type) env symbol (fun ast (a, b, c, d) -> check ast a b c d; mk (Type.parse_ty env a) (Type.parse_ty env b) (Type.parse_ty env c) (Type.parse_ty env d))
let ty_app4_ast (type env) (type ty) (module Type : Tff_intf.S with type env = env and type Ty.t = ty) ?(check=(fun _ _ _ _ _ -> ())) env symbol mk = make_op4 (module Type) env symbol (fun ast (a, b, c, d) -> check ast a b c d; mk ast (Type.parse_ty env a) (Type.parse_ty env b) (Type.parse_ty env c) (Type.parse_ty env d))
let term_app4 (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) ?(check=(fun _ _ _ _ _ -> ())) env symbol mk = make_op4 (module Type) env symbol (fun ast (a, b, c, d) -> check ast a b c d; mk (Type.parse_term env a) (Type.parse_term env b) (Type.parse_term env c) (Type.parse_term env d))
let term_app4_ast (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) ?(check=(fun _ _ _ _ _ -> ())) env symbol mk = make_op4 (module Type) env symbol (fun ast (a, b, c, d) -> check ast a b c d; mk ast (Type.parse_term env a) (Type.parse_term env b) (Type.parse_term env c) (Type.parse_term env d))
(* N-ary application *)
let term_app_list (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) ?(check=(fun _ -> ())) env _symbol mk = (fun _ast args -> List.iter check args; mk (List.map (Type.parse_term env) args) )
let term_app_list_ast (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) ?(check=(fun _ -> ())) env _symbol mk = (fun ast args -> List.iter check args; mk ast (List.map (Type.parse_term env) args) )
(* Left associative applications *)
let term_app_left (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) ?(check=(fun _ _ -> ())) env symbol mk = make_assoc (module Type) env symbol (fun ast l -> check ast l; fold_left_assoc mk (List.map (Type.parse_term env) l))
let term_app_left' (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) env symbol mk = make_assoc' (module Type) env symbol (fun _ast f l -> fold_left_assoc mk (f :: (List.map (Type.parse_term env) l)))
let term_app_left_ast (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) ?(check=(fun _ _ -> ())) env symbol mk = make_assoc (module Type) env symbol (fun ast l -> check ast l; fold_left_assoc (mk ast) (List.map (Type.parse_term env) l))
(* Right associative applications *)
let ty_app_right (type env) (type ty) (module Type : Tff_intf.S with type env = env and type Ty.t = ty) ?(check=(fun _ _ -> ())) env symbol mk = make_assoc (module Type) env symbol (fun ast l -> check ast l; fold_right_assoc mk (List.map (Type.parse_ty env) l))
let term_app_right (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) ?(check=(fun _ _ -> ())) env symbol mk = make_assoc (module Type) env symbol (fun ast l -> check ast l; fold_right_assoc mk (List.map (Type.parse_term env) l))
let term_app_right_ast (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) ?(check=(fun _ _ -> ())) env symbol mk = make_assoc (module Type) env symbol (fun ast l -> check ast l; fold_right_assoc (mk ast) (List.map (Type.parse_term env) l))
(* Chained applications *)
let term_app_chain (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) ?(check=(fun _ _ -> ())) env symbol mk = make_chain (module Type) env symbol (fun ast l -> check ast l; let l' = List.map (Type.parse_term env) l in map_chain (module Type) mk l' )
let term_app_chain_ast (type env) (type term) (module Type : Tff_intf.S with type env = env and type T.t = term) ?(check=(fun _ _ -> ())) env symbol mk = make_chain (module Type) env symbol (fun ast l -> check ast l; let l' = List.map (Type.parse_term env) l in map_chain (module Type) (mk ast) l' )
(* Higher-order application *)
let term_app_cst (type env) (type term) (type cst) (module Type : Tff_intf.S with type env = env and type T.t = term and type T.Const.t = cst) env cst = fun ast args -> Type.unwrap_term env ast (Type.parse_app_term_cst env ast cst args)
let term_app_ho (type env) (type term) (module Type : Thf_intf.S with type env = env and type T.t = term) env f = fun ast args -> Type.unwrap_term env ast (Type.parse_app_ho_term env ast f args)
let term_app_ho_ast (type env) (type term) (module Type : Thf_intf.S with type env = env and type T.t = term) env f = fun ast args -> Type.unwrap_term env ast (Type.parse_app_ho_term env ast (f ast) args)