reduction_engine.mli 1.29 KB
Newer Older
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


(*********************

{1 A reduction engine for Why3 terms}

*************************)

(*
terms are normalized with respect to

1) built-in computation rules

 a) on propositional connectives, e.g.

   f /\ true -> f

 b) on integers, e.g.

   35 + 7 -> 42

 c) on projections of pairs and of other ADTs, e.g

  fst (x,y) -> x

  cdr (Cons x y) -> y

 d) on defined function symbols, e.g.

  function sqr (x:int) = x * x

  sqr 4 -> 4 * 4 -> 16

  sqr x -> x * x

 e) (TODO?) on booleans, e.g.

  True xor False -> True

 f) (TODO?) on reals, e.g.

  1.0 + 2.5 -> 3.5

2) axioms declared as rewrite rules, thanks to the "rewrite" metas, e.g. if

    function dot : t -> t -> t
    axiom assoc: forall x y z, dot (dot x y) z = dot x (dot y z)
    meta "rewrite" assoc

  then

  dot (dot a b) (dot c d) -> dot a (dot b (dot c d))

  axioms used as rewrite rules must be either of the form

    forall ... t1 = t2

  or

    forall ... f1 <-> f2

   where the root symbol of t1 (resp. f1) is a non-interpreted function
   symbol (resp. non-interpreted predicate symbol)

  rewriting is done from left to right


*)

type engine

72
val create : Env.env -> Decl.decl Ident.Mid.t -> engine
73
74
75
76
77

exception NotARewriteRule of string

val add_rule : Term.term -> engine -> engine

78
79
80
81
82


val normalize : engine -> Term.term -> Term.term