blob: 33f71ab785e8f45033f88b5bd099d6223de5de8b (
plain)
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
|
(*Generated by Lem from string_extra.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_numTheory lem_listTheory lem_basic_classesTheory lem_stringTheory lem_list_extraTheory ASCIInumbersTheory stringLib;
val _ = numLib.prefer_num();
val _ = new_theory "lem_string_extra"
(******************************************************************************)
(* String functions *)
(******************************************************************************)
(*open import Basic_classes*)
(*open import Num*)
(*open import List*)
(*open import String*)
(*open import List_extra*)
(*open import {hol} `stringLib`*)
(*open import {hol} `ASCIInumbersTheory`*)
(******************************************************************************)
(* Character's to numbers *)
(******************************************************************************)
(*val ord : char -> nat*)
(*val chr : nat -> char*)
(******************************************************************************)
(* Converting to strings *)
(******************************************************************************)
(*val stringFromNatHelper : nat -> list char -> list char*)
val stringFromNatHelper_defn = Hol_defn "stringFromNatHelper" `
((stringFromNatHelper:num ->(char)list ->(char)list) n acc=
(if n =( 0 : num) then
acc
else
stringFromNatHelper (n DIV( 10 : num)) (CHR ((n MOD( 10 : num)) +( 48 : num)) :: acc)))`;
val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn stringFromNatHelper_defn;
(*val stringFromNat : nat -> string*)
(*val stringFromNaturalHelper : natural -> list char -> list char*)
val stringFromNaturalHelper_defn = Hol_defn "stringFromNaturalHelper" `
((stringFromNaturalHelper:num ->(char)list ->(char)list) n acc=
(if n =( 0:num) then
acc
else
stringFromNaturalHelper (n DIV( 10:num)) (CHR ((((n MOD( 10:num)) +( 48:num)):num)) :: acc)))`;
val _ = Lib.with_flag (computeLib.auto_import_definitions, false) Defn.save_defn stringFromNaturalHelper_defn;
(*val stringFromNatural : natural -> string*)
(*val stringFromInt : int -> string*)
val _ = Define `
((stringFromInt:int -> string) i=
(if i <( 0 : int) then
STRCAT"-" (num_to_dec_string (Num (ABS i)))
else
num_to_dec_string (Num (ABS i))))`;
(*val stringFromInteger : integer -> string*)
val _ = Define `
((stringFromInteger:int -> string) i=
(if i <( 0 : int) then
STRCAT"-" (num_to_dec_string (Num (ABS i)))
else
num_to_dec_string (Num (ABS i))))`;
(******************************************************************************)
(* List-like operations *)
(******************************************************************************)
(*val nth : string -> nat -> char*)
(*let nth s n= List_extra.nth (toCharList s) n*)
(*val stringConcat : list string -> string*)
(*let stringConcat s=
List.foldr (^) "" s*)
(******************************************************************************)
(* String comparison *)
(******************************************************************************)
(*val stringCompare : string -> string -> ordering*)
val _ = Define `
((stringLess:string -> string -> bool) x y= (orderingIsLess (EQUAL)))`;
val _ = Define `
((stringLessEq:string -> string -> bool) x y= (~ (orderingIsGreater (EQUAL))))`;
val _ = Define `
((stringGreater:string -> string -> bool) x y= (stringLess y x))`;
val _ = Define `
((stringGreaterEq:string -> string -> bool) x y= (stringLessEq y x))`;
val _ = Define `
((instance_Basic_classes_Ord_string_dict:(string)Ord_class)= (<|
compare_method := (\ x y. EQUAL);
isLess_method := stringLess;
isLessEqual_method := stringLessEq;
isGreater_method := stringGreater;
isGreaterEqual_method := stringGreaterEq|>))`;
val _ = export_theory()
|
