Source file normalize.ml

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

(* This file is free software, part of dolmen. See file "LICENSE" for more information. *)

module Tptp = struct

  let symbol m ~attr ~loc id =
    let t = match id with
      (* Base builtins *)
      | { Id.name =  "$_"; ns = Id.Term }     -> Term.(builtin ?loc Wildcard ())
      | { Id.name = "$tType" ; ns = Id.Term } -> Term.(builtin ?loc Ttype ())
      | { Id.name = "$o"; ns = Id.Term }      -> Term.(builtin ?loc Prop ())
      | { Id.name = "$true"; ns = Id.Term }   -> Term.(builtin ?loc True ())
      | { Id.name = "$false"; ns = Id.Term }  -> Term.(builtin ?loc False ())
      (* Arithmetic builtins *)
      | { Id.name = "$int"; ns = Id.Term }        -> Term.(builtin ?loc Int ())
      | { Id.name = "$less"; ns = Id.Term }       -> Term.(builtin ?loc Lt ())
      | { Id.name = "$lesseq"; ns = Id.Term }     -> Term.(builtin ?loc Leq ())
      | { Id.name = "$greater"; ns = Id.Term }    -> Term.(builtin ?loc Gt ())
      | { Id.name = "$greatereq"; ns = Id.Term }  -> Term.(builtin ?loc Geq ())
      | { Id.name = "$uminus"; ns = Id.Term }     -> Term.(builtin ?loc Minus ())
      | { Id.name = "$sum"; ns = Id.Term }        -> Term.(builtin ?loc Add ())
      | { Id.name = "$difference"; ns = Id.Term } -> Term.(builtin ?loc Sub ())
      | { Id.name = "$product"; ns = Id.Term }    -> Term.(builtin ?loc Mult ())
      | _ -> Term.(const ?loc id)
    in
    let attrs = List.map (Term.map m) attr in
    Term.add_attrs attrs t

  let mapper =
    { Term.id_mapper with symbol }

end

module Smtlib = struct

  let symbol m ~attr ~loc id =
    let t = match id with
      | { Id.name = "Bool"; ns = Id.Sort }  -> Term.(builtin ?loc Prop ())
      | { Id.name = "true"; ns = Id.Term }  -> Term.(builtin ?loc True ())
      | { Id.name = "false"; ns = Id.Term } -> Term.(builtin ?loc False ())
      | { Id.name = "not"; ns = Id.Term }   -> Term.(builtin ?loc Not ())
      | { Id.name = "and"; ns = Id.Term }   -> Term.(builtin ?loc And ())
      | { Id.name = "or"; ns = Id.Term }    -> Term.(builtin ?loc Or ())
      | { Id.name = "xor"; ns = Id.Term }   -> Term.(builtin ?loc Xor ())
      | { Id.name = "=>"; ns = Id.Term }    -> Term.(builtin ?loc Imply ())
      | { Id.name = "="; ns = Id.Term }     -> Term.(builtin ?loc Eq ())
      | { Id.name = "distinct"; ns = Id.Term } -> Term.(builtin ?loc Distinct ())
      | { Id.name = "ite"; ns = Id.Term }   -> Term.(builtin ?loc Ite ())
      | _ -> Term.(const ?loc id)
    in
    let attrs = List.map (Term.map m) attr in
    Term.add_attrs attrs t

  let binder_let_eq m t =
    match t with
    | { Term.term = Term.Colon (u, v) ; _ } ->
      Term.eq ?loc:t.Term.loc (Term.map m u) (Term.map m v)
    | _ -> assert false

  let binder m ~attr ~loc b l body =
    match b with
    | Term.Let ->
      let attrs = List.map (Term.map m) attr in
      let l' = List.map (binder_let_eq m) l in
      Term.add_attrs attrs (Term.letin ?loc l' (Term.map m body))
    | _ -> Term.(id_mapper.binder m ~attr ~loc b l body)

  let mapper =
    { Term.id_mapper with symbol; binder }

end