Commit e535be60 authored by Andrei Paskevich's avatar Andrei Paskevich

move non-core term/fmla functions to Termlib

parent 1a78e107
......@@ -104,8 +104,8 @@ doc/version.tex src/version.ml: Version version.sh config.status
# why
#####
CORE_CMO := ident.cmo ty.cmo term.cmo theory.cmo pretty.cmo \
transform.cmo context_utils.cmo
CORE_CMO := ident.cmo ty.cmo term.cmo termlib.cmo theory.cmo \
pretty.cmo transform.cmo context_utils.cmo
CORE_CMO := $(addprefix src/core/,$(CORE_CMO))
UTIL_CMO := pp.cmo loc.cmo util.cmo hashcons.cmo
......@@ -115,7 +115,7 @@ PARSER_CMO := parser.cmo lexer.cmo typing.cmo transform_utils.cmo
PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))
TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo \
flatten.cmo
flatten.cmo
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
OUTPUT_CMO := driver_parser.cmo driver_lexer.cmo driver.cmo \
......
This diff is collapsed.
......@@ -87,10 +87,6 @@ val pat_fold : ('a -> pattern -> 'a) -> 'a -> pattern -> 'a
val pat_all : (pattern -> bool) -> pattern -> bool
val pat_any : (pattern -> bool) -> pattern -> bool
(* equality modulo alpha *)
val pat_equal_alpha : pattern -> pattern -> bool
(** Terms and formulas *)
type label = string
......@@ -178,6 +174,7 @@ val t_eps : vsymbol -> fmla -> term
val t_label : label list -> term -> term
val t_label_add : label -> term -> term
val t_label_copy : term -> term -> term
(* smart constructors for fmla *)
......@@ -199,13 +196,14 @@ val f_case : term -> (pattern * fmla) list -> fmla
val f_label : label list -> fmla -> fmla
val f_label_add : label -> fmla -> fmla
val f_label_copy : fmla -> fmla -> fmla
(* bindings *)
(* open bindings *)
val t_open_bound : term_bound -> vsymbol * term
val t_open_branch : term_branch -> pattern * Svs.t * term
val f_open_bound : fmla_bound -> vsymbol * fmla
val t_open_branch : term_branch -> pattern * Svs.t * term
val f_open_branch : fmla_branch -> pattern * Svs.t * fmla
val f_open_quant : fmla_quant -> vsymbol list * trigger list * fmla
......@@ -213,6 +211,20 @@ val f_open_quant : fmla_quant -> vsymbol list * trigger list * fmla
val f_open_forall : fmla -> vsymbol list * fmla
val f_open_exists : fmla -> vsymbol list * fmla
(* unsafe open with unprotected de Bruijn indices *)
val t_open_bound_unsafe : term_bound -> vsymbol * term
val f_open_bound_unsafe : fmla_bound -> vsymbol * fmla
val t_open_branch_unsafe : term_branch -> pattern * int * term
val f_open_branch_unsafe : fmla_branch -> pattern * int * fmla
val f_open_quant_unsafe :
fmla_quant -> vsymbol list * int * trigger list * fmla
val f_open_forall_unsafe : fmla -> vsymbol list * int * fmla
val f_open_exists_unsafe : fmla -> vsymbol list * int * fmla
(* unsafe traversal with unprotected de Bruijn indices *)
val t_map_unsafe : (int -> term -> term) ->
......@@ -239,25 +251,13 @@ val t_any_unsafe : (int -> term -> bool) ->
val f_any_unsafe : (int -> term -> bool) ->
(int -> fmla -> bool) -> int -> fmla -> bool
(* generic term/fmla traversal *)
val t_map : (term -> term) -> (fmla -> fmla) -> term -> term
val f_map : (term -> term) -> (fmla -> fmla) -> fmla -> fmla
val t_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> term -> 'a
val f_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> fmla -> 'a
val t_all : (term -> bool) -> (fmla -> bool) -> term -> bool
val f_all : (term -> bool) -> (fmla -> bool) -> fmla -> bool
val t_any : (term -> bool) -> (fmla -> bool) -> term -> bool
val f_any : (term -> bool) -> (fmla -> bool) -> fmla -> bool
(* trigger traversal *)
val tr_map : (term -> term) -> (fmla -> fmla) -> trigger list -> trigger list
val tr_map : (term -> term) ->
(fmla -> fmla) -> trigger list -> trigger list
val tr_fold :
('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> trigger list -> 'a
val tr_fold : ('a -> term -> 'a) ->
('a -> fmla -> 'a) -> 'a -> trigger list -> 'a
(* map/fold over symbols *)
......@@ -275,74 +275,6 @@ val f_s_all : (tysymbol -> bool) -> (lsymbol -> bool) -> fmla -> bool
val t_s_any : (tysymbol -> bool) -> (lsymbol -> bool) -> term -> bool
val f_s_any : (tysymbol -> bool) -> (lsymbol -> bool) -> fmla -> bool
(* map/fold over free variables *)
val t_v_map : (vsymbol -> term) -> term -> term
val f_v_map : (vsymbol -> term) -> fmla -> fmla
val t_v_fold : ('a -> vsymbol -> 'a) -> 'a -> term -> 'a
val f_v_fold : ('a -> vsymbol -> 'a) -> 'a -> fmla -> 'a
val t_v_all : (vsymbol -> bool) -> term -> bool
val f_v_all : (vsymbol -> bool) -> fmla -> bool
val t_v_any : (vsymbol -> bool) -> term -> bool
val f_v_any : (vsymbol -> bool) -> fmla -> bool
(* variable occurrence check *)
val t_occurs : Svs.t -> term -> bool
val f_occurs : Svs.t -> fmla -> bool
val t_occurs_single : vsymbol -> term -> bool
val f_occurs_single : vsymbol -> fmla -> bool
(* substitution for variables *)
val t_subst : term Mvs.t -> term -> term
val f_subst : term Mvs.t -> fmla -> fmla
val t_subst_single : vsymbol -> term -> term -> term
val f_subst_single : vsymbol -> term -> fmla -> fmla
(* set of free variables *)
val t_freevars : Svs.t -> term -> Svs.t
val f_freevars : Svs.t -> fmla -> Svs.t
(* equality modulo alpha *)
val t_equal_alpha : term -> term -> bool
val f_equal_alpha : fmla -> fmla -> bool
(* occurrence check *)
val t_occurs_term : term -> term -> bool
val f_occurs_term : term -> fmla -> bool
val t_occurs_fmla : fmla -> term -> bool
val f_occurs_fmla : fmla -> fmla -> bool
val t_occurs_term_alpha : term -> term -> bool
val f_occurs_term_alpha : term -> fmla -> bool
val t_occurs_fmla_alpha : fmla -> term -> bool
val f_occurs_fmla_alpha : fmla -> fmla -> bool
(* term/fmla replacement *)
val t_subst_term : term -> term -> term -> term
val f_subst_term : term -> term -> fmla -> fmla
val t_subst_fmla : fmla -> fmla -> term -> term
val f_subst_fmla : fmla -> fmla -> fmla -> fmla
val t_subst_term_alpha : term -> term -> term -> term
val f_subst_term_alpha : term -> term -> fmla -> fmla
val t_subst_fmla_alpha : fmla -> fmla -> term -> term
val f_subst_fmla_alpha : fmla -> fmla -> fmla -> fmla
(* term/fmla matching modulo alpha in the pattern *)
val t_match : term -> term -> term Mvs.t -> term Mvs.t option
val f_match : fmla -> fmla -> term Mvs.t -> term Mvs.t option
(* built-in symbols *)
val ps_equ : lsymbol
......
This diff is collapsed.
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Ident
open Ty
open Term
(* generic term/fmla traversal *)
val t_map : (term -> term) -> (fmla -> fmla) -> term -> term
val f_map : (term -> term) -> (fmla -> fmla) -> fmla -> fmla
val t_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> term -> 'a
val f_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> fmla -> 'a
val t_all : (term -> bool) -> (fmla -> bool) -> term -> bool
val f_all : (term -> bool) -> (fmla -> bool) -> fmla -> bool
val t_any : (term -> bool) -> (fmla -> bool) -> term -> bool
val f_any : (term -> bool) -> (fmla -> bool) -> fmla -> bool
(* map/fold over free variables *)
val t_v_map : (vsymbol -> term) -> term -> term
val f_v_map : (vsymbol -> term) -> fmla -> fmla
val t_v_fold : ('a -> vsymbol -> 'a) -> 'a -> term -> 'a
val f_v_fold : ('a -> vsymbol -> 'a) -> 'a -> fmla -> 'a
val t_v_all : (vsymbol -> bool) -> term -> bool
val f_v_all : (vsymbol -> bool) -> fmla -> bool
val t_v_any : (vsymbol -> bool) -> term -> bool
val f_v_any : (vsymbol -> bool) -> fmla -> bool
(* variable occurrence check *)
val t_occurs : Svs.t -> term -> bool
val f_occurs : Svs.t -> fmla -> bool
val t_occurs_single : vsymbol -> term -> bool
val f_occurs_single : vsymbol -> fmla -> bool
(* substitution for variables *)
val t_subst : term Mvs.t -> term -> term
val f_subst : term Mvs.t -> fmla -> fmla
val t_subst_single : vsymbol -> term -> term -> term
val f_subst_single : vsymbol -> term -> fmla -> fmla
(* set of free variables *)
val t_freevars : Svs.t -> term -> Svs.t
val f_freevars : Svs.t -> fmla -> Svs.t
(* equality modulo alpha *)
val t_equal_alpha : term -> term -> bool
val f_equal_alpha : fmla -> fmla -> bool
(* occurrence check *)
val t_occurs_term : term -> term -> bool
val f_occurs_term : term -> fmla -> bool
val t_occurs_fmla : fmla -> term -> bool
val f_occurs_fmla : fmla -> fmla -> bool
val t_occurs_term_alpha : term -> term -> bool
val f_occurs_term_alpha : term -> fmla -> bool
val t_occurs_fmla_alpha : fmla -> term -> bool
val f_occurs_fmla_alpha : fmla -> fmla -> bool
(* term/fmla replacement *)
val t_subst_term : term -> term -> term -> term
val f_subst_term : term -> term -> fmla -> fmla
val t_subst_fmla : fmla -> fmla -> term -> term
val f_subst_fmla : fmla -> fmla -> fmla -> fmla
val t_subst_term_alpha : term -> term -> term -> term
val f_subst_term_alpha : term -> term -> fmla -> fmla
val t_subst_fmla_alpha : fmla -> fmla -> term -> term
val f_subst_fmla_alpha : fmla -> fmla -> fmla -> fmla
(* term/fmla matching modulo alpha in the pattern *)
val t_match : term -> term -> term Mvs.t -> term Mvs.t option
val f_match : fmla -> fmla -> term Mvs.t -> term Mvs.t option
......@@ -22,6 +22,7 @@ open Util
open Ident
open Ty
open Term
open Termlib
(** Named propositions *)
......
......@@ -19,6 +19,7 @@
open Ident
open Term
open Termlib
open Theory
open Context
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment