]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_transformations/contentTable.ml
added reference to MetadataQuery (now it builds properly)
[helm.git] / helm / ocaml / cic_transformations / contentTable.ml
1
2 (* NOTATION *)
3
4 let symbol_table = Hashtbl.create 503 ;;
5 let lookup_symbol = Hashtbl.find symbol_table ;;
6
7 let idref id t = CicAst.AttributedTerm (`IdRef id, t) ;;
8
9 let add_symbol uri mnemonic =
10   Hashtbl.add symbol_table uri
11     (fun aid sid args ast_of_acic ->
12       idref aid (CicAst.Appl
13         (idref sid (CicAst.Symbol (mnemonic, 0)) :: List.map ast_of_acic args)))
14 ;;
15
16 (* eq *)
17 Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI
18   (fun aid sid args ast_of_acic ->
19     idref aid (CicAst.Appl
20       (idref sid (CicAst.Symbol ("eq", 0)) ::
21         List.map ast_of_acic (List.tl args)))) ;;
22
23 (* and *)
24 add_symbol HelmLibraryObjects.Logic.and_XURI "and" ;;
25
26 (* or *)
27 add_symbol HelmLibraryObjects.Logic.or_XURI "or" ;;
28
29 (* iff *)
30 add_symbol HelmLibraryObjects.Logic.iff_SURI "iff" ;;
31
32 (* not *)
33 add_symbol HelmLibraryObjects.Logic.not_SURI "not" ;;
34
35 (* Rinv *)
36 add_symbol HelmLibraryObjects.Reals.rinv_SURI "inv" ;;
37
38 (* Ropp *)
39 add_symbol HelmLibraryObjects.Reals.ropp_SURI "opp" ;;
40
41 (* exists *)
42 Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI
43   (fun aid sid args ast_of_acic ->
44    match (List.tl args) with
45      [Cic.ALambda (_,n,s,t)] ->
46        idref aid
47         (CicAst.Binder (`Exists, (n, Some (ast_of_acic s)), ast_of_acic t))
48   | _ -> raise Not_found);;
49
50 (* leq *) 
51 add_symbol HelmLibraryObjects.Peano.le_XURI "leq" ;;
52 add_symbol HelmLibraryObjects.Reals.rle_SURI "leq" ;;
53
54 (* lt *)
55 add_symbol HelmLibraryObjects.Peano.lt_SURI "lt" ;;
56 add_symbol HelmLibraryObjects.Reals.rlt_SURI "lt" ;;
57
58 (* geq *)
59 add_symbol HelmLibraryObjects.Peano.ge_SURI "geq" ;;
60 add_symbol HelmLibraryObjects.Reals.rge_SURI "geq" ;;
61
62 (* gt *)
63 add_symbol HelmLibraryObjects.Peano.gt_SURI "gt" ;;
64 add_symbol HelmLibraryObjects.Reals.rgt_SURI "gt" ;;
65
66 (* plus *)
67 add_symbol HelmLibraryObjects.Peano.plus_SURI "plus" ;;
68 add_symbol HelmLibraryObjects.BinInt.zplus_SURI "plus" ;;
69
70 let rplus_uri = HelmLibraryObjects.Reals.rplus_URI;;
71 let r1_uri = HelmLibraryObjects.Reals.r1_URI;;
72
73 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI
74   (fun aid sid args ast_of_acic ->
75     let appl () =
76       idref aid (CicAst.Appl 
77         (idref sid (CicAst.Symbol ("plus", 0)) :: List.map ast_of_acic args))
78    in
79     let rec aux acc = function
80       | [ Cic.AConst (nid, uri, []); n] when UriManager.eq uri r1_uri ->
81             (match n with
82             | Cic.AConst (_, uri, []) when UriManager.eq uri r1_uri ->
83                 idref aid (CicAst.Num (string_of_int (acc+2), 0))
84             | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args)
85               when UriManager.eq uri rplus_uri ->
86                 aux (acc + 1) args
87             | _ -> appl ())
88       | _ -> appl ()
89     in
90     aux 0 args)
91 ;;
92
93 (* zero and one *)
94 Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI
95   (fun _ sid _ _ -> idref sid (CicAst.Num ("0", 0))) ;;
96 Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
97   (fun _ sid _ _ -> idref sid (CicAst.Num ("1", 0))) ;;
98
99 (* times *) 
100 add_symbol HelmLibraryObjects.Peano.mult_SURI "times" ;;
101 add_symbol HelmLibraryObjects.Reals.rmult_SURI "times" ;;
102
103 (* minus *)
104 add_symbol HelmLibraryObjects.Peano.minus_SURI "minus" ;;
105 add_symbol HelmLibraryObjects.Reals.rminus_SURI "minus" ;;
106
107 (* div *)
108 add_symbol HelmLibraryObjects.Reals.rdiv_SURI "div" ;;
109