candle/hol_lib.ml at master · CakeML/candle · GitHub

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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
(* ========================================================================= *)
(*                               HOL LIGHT                                   *)
(*                                                                           *)
(*              Modern OCaml version of the HOL theorem prover               *)
(*                                                                           *)
(*                            John Harrison                                  *)
(*                                                                           *)
(*            (c) Copyright, University of Cambridge 1998                    *)
(*              (c) Copyright, John Harrison 1998-2024                       *)
(*              (c) Copyright, Juneyoung Lee 2024                            *)
(* ========================================================================= *)

(*
include Bignum;;
open Hol_loader;;
*)

(* ------------------------------------------------------------------------- *)
(* Make it harder to accidentally use CakeML-specific code and add a         *)
(* compatiblity layer.                                                       *)
(* ------------------------------------------------------------------------- *)

loads "candle/build/insulate.ml";;  (* Moves CakeML specifics.               *)
loads "candle/nums.ml";;            (* Load "num".                           *)
loads "candle/pretty.ml";;          (* Pretty printer code.                  *)
loads "candle/ocaml.ml";;           (* OCaml modules.                        *)

(* ------------------------------------------------------------------------- *)
(* Bind these to names that are independent of OCaml versions before they    *)
(* are potentially overwritten by an identifier of the same name. In older   *)
(* and newer Ocaml versions these are respectively:                          *)
(*                                                                           *)
(* Pervasives.sqrt -> Float.sqrt                                             *)
(* Pervasives.abs_float -> Stdlib.abs_float / Float.abs                      *)
(* ------------------------------------------------------------------------- *)

let float_sqrt = Float.sqrt;;
let float_fabs = Float.abs;;

(* ------------------------------------------------------------------------- *)
(* Various tweaks to OCaml and general library functions.                    *)
(* ------------------------------------------------------------------------- *)

loads "system.ml";;        (* Set up proper parsing                          *)
loads "bignum_num.ml";;    (* Load bignums                                   *)
loads "lib.ml";;           (* Various useful general library functions       *)

(* ------------------------------------------------------------------------- *)
(* Candle things.                                                            *)
(* ------------------------------------------------------------------------- *)

loads "candle/kernel.ml";;               (* Brings Candle kernel into scope. *)

(* ------------------------------------------------------------------------- *)
(* Some extra support stuff needed outside the core.                         *)
(* ------------------------------------------------------------------------- *)

loads "basics.ml";;     (* Additional syntax operations and other utilities  *)
loads "nets.ml";;       (* Term nets for fast matchability-based lookup      *)

(* ------------------------------------------------------------------------- *)
(* The interface.                                                            *)
(* ------------------------------------------------------------------------- *)

loads "printer.ml";;    (* Crude prettyprinter                               *)
loads "preterm.ml";;    (* Preterms and their interconversion with terms     *)
loads "parser.ml";;     (* Lexer and parser                                  *)

(* ------------------------------------------------------------------------- *)
(* Higher level deductive system.                                            *)
(* ------------------------------------------------------------------------- *)

loads "equal.ml";;      (* Basic equality reasoning and conversionals        *)
loads "bool.ml";;       (* Boolean theory and basic derived rules            *)
loads "drule.ml";;      (* Additional derived rules                          *)
loads "tactics.ml";;    (* Tactics, tacticals and goal stack                 *)
loads "itab.ml";;       (* Toy prover for intuitionistic logic               *)
loads "simp.ml";;       (* Basic rewriting and simplification tools          *)
loads "theorems.ml";;   (* Additional theorems (mainly for quantifiers) etc. *)
loads "ind_defs.ml";;   (* Derived rules for inductive definitions           *)
loads "class.ml";;      (* Classical reasoning: Choice and Extensionality    *)
loads "trivia.ml";;     (* Some very basic theories, e.g. type ":1"          *)
loads "canon.ml";;      (* Tools for putting terms in canonical forms        *)
loads "meson.ml";;      (* First order automation: MESON (model elimination) *)
loads "firstorder.ml";; (* More utilities for first-order shadow terms       *)
loads "metis.ml";;      (* More advanced first-order automation: Metis       *)
(*
loads "thecops.ml";;    (* Connection-based automation: leanCoP and nanoCoP  *)
*)
loads "quot.ml";;       (* Derived rules for defining quotient types         *)
loads "impconv.ml";;    (* More powerful implicational rewriting etc.        *)

(* ------------------------------------------------------------------------- *)
(* Mathematical theories and additional proof tools.                         *)
(* ------------------------------------------------------------------------- *)

loads "pair.ml";;       (* Theory of pairs                                   *)
loads "compute.ml";;    (* General call-by-value reduction tool for terms    *)
loads "nums.ml";;       (* Axiom of Infinity, definition of natural numbers  *)
loads "recursion.ml";;  (* Tools for primitive recursion on inductive types  *)
loads "arith.ml";;      (* Natural number arithmetic                         *)
loads "wf.ml";;         (* Theory of wellfounded relations                   *)
loads "calc_num.ml";;   (* Calculation with natural numbers                  *)
loads "normalizer.ml";; (* Polynomial normalizer for rings and semirings     *)
loads "grobner.ml";;    (* Groebner basis procedure for most semirings       *)
loads "ind_types.ml";;  (* Tools for defining inductive types                *)
loads "lists.ml";;      (* Theory of lists                                   *)
loads "realax.ml";;     (* Definition of real numbers                        *)
loads "calc_int.ml";;   (* Calculation with integer-valued reals             *)
loads "realarith.ml";;  (* Universal linear real decision procedure          *)
loads "real.ml";;       (* Derived properties of reals                       *)
loads "calc_rat.ml";;   (* Calculation with rational-valued reals            *)
loads "int.ml";;        (* Definition of integers                            *)
loads "sets.ml";;       (* Basic set theory                                  *)
loads "iterate.ml";;    (* Iterated operations                               *)
loads "cart.ml";;       (* Finite Cartesian products                         *)
loads "define.ml";;     (* Support for general recursive definitions         *)

(* ------------------------------------------------------------------------- *)
(* In-logic computation function.                                            *)
(* ------------------------------------------------------------------------- *)

loads "candle/compute.ml";; (* Definitions of cval primitives                *)

(* ------------------------------------------------------------------------- *)
(* Checks that no axiom other than those allowed by core libs are introduced *)
(* ------------------------------------------------------------------------- *)

let check_axioms () =
  let basic_axioms = [INFINITY_AX; SELECT_AX; ETA_AX] in
  let l = filter (fun th -> not (mem th basic_axioms)) (axioms()) in
  if l <> [] then
    let msg = "[" ^ (String.concat ", " (map string_of_thm l)) ^ "]" in
    failwith ("check_axioms: " ^ msg);;