simple_term_rewriter 0.3.0

A basic interface to rewrite concrete tree terms according to a set of rules
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97

/*
Copyright 2024 Erwan Mahe (github.com/erwanM974)

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*/


use crate::core::terms::{position::PositionInLanguageTerm, term::{LanguageTerm, RewritableLanguageOperatorSymbol}};


/**
 Something that can simplify a term which root is a unary operator.
 **/
pub trait GenericUnaryOperatorSimplifier<LOS : RewritableLanguageOperatorSymbol> {
    fn is_unary(&self, op : &LOS) -> bool;

    /**
     Try to simplify a term which root is a unary operator.
    This can be used to:
        - simplify fixed points under unary operators
        - merge nested unary operators
    More complex cases can also be implemented via this trait.
    Examples :
    - in integer computation : try_compose_nested_unary_operators( .^3 , 1 ) will return Some(1) because 1
      is a fixed point for the power operator
    - in sequence diagrams : try_compose_nested_unary_operators( loop, assert(i) ) will return None because it is not possible to
      merge a "loop" and an "assert"
    - in integer computation : try_compose_nested_unary_operators( .^3 , x^5 ) will return Some(Some(x^8)) because,
      we can compose the power operators
    - in boolean logic : try_compose_nested_unary_operators( ¬ , ¬(x) ) will return Some(x) because, because,
      we if we compose ¬ and ¬, we get the identity operator
     **/
    fn try_simplify_under_unary_operator(
        &self,
        top_operator : &LOS,
        term_underneath : &LanguageTerm<LOS>
    ) -> Option<LanguageTerm<LOS>>;
}




/**
 *  This can be used to simplify a term which has a unary operator at its root.
 *  Two examples below.
 *  
 *  (1) If op and op' are two unary operators and if there exists
 *  an op'' such that for any x, op(op'(x)) is equivalent to op''(x)
 *  then we may rewrite :
 *  op(op'(x)) -> op''(x)
 *  
 *  A typical example of that is the power operation on real numbers:
 *  we have, for any reals y and z:
 *  - denoting the operator x->x^y as F
 *  - denoting the operator x->x^z as G
 *  - denoting the operator x->x^(y+z) as H
 * 
 *  We have, for any real x G(F(x)) = H(x) so we may perform the rewrite operation:
 *  G(F(x)) -> H(x)
 *  which is semantically correct
 *  
 *  (2) If c is a constant (operator with arity 0) and it is a fixpoint for a unary operator op
 *  then we may rewrite :
 *  - op(c) -> c
 *  
 * A typical example of that is fixpoints for unary operators, for example:
 * - for any real x, 1^x = 1
 **/
pub(crate) fn transformation_generic_simpl_under_unary_operator<
    LOS : RewritableLanguageOperatorSymbol
>(
    checker : &Box<dyn GenericUnaryOperatorSimplifier<LOS>>,
    term : &LanguageTerm<LOS>,
    _context_term : &LanguageTerm<LOS>,
    _position_in_context_term : &PositionInLanguageTerm
) -> Option<LanguageTerm<LOS>> {
    let operator_at_root = &term.operator;

    if checker.is_unary(operator_at_root) {
        let sub_term = term.sub_terms.first().unwrap();
        checker.try_simplify_under_unary_operator(operator_at_root, sub_term)
    } else {
        None
    }
}