max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/data/string): remove string_imp

Browse source 
We will use the (to be implemented) `opaque` keyword
This commit is contained in:
Leonardo de Moura 2018-10-01 13:02:32 -07:00
parent 81e9e95570
commit 3a4acbee9e
2 changed files with 16 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
library/init/data/string/basic.lean
View file

@ -9,19 +9,14 @@ import init.data.char.basic
import init.data.option.basic
/- In the VM, strings are implemented using a dynamic array and UTF-8 encoding.
TODO: we currently cannot mark string_imp as private because
we need to bind string_imp.mk and string_imp.cases_on in the VM.
-/
structure string_imp :=
TODO: mark as opaque -/
structure string :=
(data : list char)
def string := string_imp
instance : decidable_eq string :=
{dec_eq := λ ⟨s₁⟩ ⟨s₂⟩,
if h : s₁ = s₂ then is_true (congr_arg _ h)
else is_false (λ h', string_imp.no_confusion h' (λ h', absurd h' h))}
else is_false (λ h', string.no_confusion h' (λ h', absurd h' h))}
def list.as_string (s : list char) : string :=
⟨s⟩
@ -265,8 +260,8 @@ private lemma nil_ne_append_singleton : ∀ (c : char) (l : list char), [] ≠ l
lemma empty_ne_str : ∀ (c : char) (s : string), empty ≠ str s c
| c ⟨l⟩ :=
λ h : string_imp.mk [] = string_imp.mk (l ++ [c]),
string_imp.no_confusion h $ λ h, nil_ne_append_singleton _ _ h
λ h : string.mk [] = string.mk (l ++ [c]),
string.no_confusion h $ λ h, nil_ne_append_singleton _ _ h
lemma str_ne_empty (c : char) (s : string) : str s c ≠ empty :=
(empty_ne_str c s).symm
@ -287,8 +282,8 @@ private lemma str_ne_str_left_aux : ∀ {c₁ c₂ : char} (l₁ l₂ : list cha
absurd this (str_ne_str_left_aux l₁ l₂ h₁)
lemma str_ne_str_left : ∀ {c₁ c₂ : char} (s₁ s₂ : string), c₁ ≠ c₂ → str s₁ c₁ ≠ str s₂ c₂
| c₁ c₂ (string_imp.mk l₁) (string_imp.mk l₂) h₁ h₂ :=
have l₁ ++ [c₁] = l₂ ++ [c₂], from string_imp.no_confusion h₂ id,
| c₁ c₂ (string.mk l₁) (string.mk l₂) h₁ h₂ :=
have l₁ ++ [c₁] = l₂ ++ [c₂], from string.no_confusion h₂ id,
absurd this (str_ne_str_left_aux l₁ l₂ h₁)
private lemma str_ne_str_right_aux : ∀ (c₁ c₂ : char) {l₁ l₂ : list char}, l₁ ≠ l₂ → l₁ ++ [c₁] ≠ l₂ ++ [c₂]
@ -311,11 +306,11 @@ private lemma str_ne_str_right_aux : ∀ (c₁ c₂ : char) {l₁ l₂ : list ch
absurd this (str_ne_str_right_aux c₁ c₂ aux₂)
lemma str_ne_str_right : ∀ (c₁ c₂ : char) {s₁ s₂ : string}, s₁ ≠ s₂ → str s₁ c₁ ≠ str s₂ c₂
| c₁ c₂ (string_imp.mk l₁) (string_imp.mk l₂) h₁ h₂ :=
| c₁ c₂ (string.mk l₁) (string.mk l₂) h₁ h₂ :=
have aux : l₁ ≠ l₂, from λ h,
have string_imp.mk l₁ = string_imp.mk l₂, from eq.subst h rfl,
have string.mk l₁ = string.mk l₂, from eq.subst h rfl,
absurd this h₁,
have l₁ ++ [c₁] = l₂ ++ [c₂], from string_imp.no_confusion h₂ id,
have l₁ ++ [c₁] = l₂ ++ [c₂], from string.no_confusion h₂ id,
absurd this (str_ne_str_right_aux c₁ c₂ aux)
end string

12
src/library/vm/vm_string.cpp
View file

@ -55,7 +55,7 @@ static pair<std::string, size_t> list_as_string(vm_obj const & lst) {
return mk_pair(s, len);
}
vm_obj string_imp_mk(vm_obj const & lst) {
vm_obj string_mk(vm_obj const & lst) {
std::string s;
size_t len;
std::tie(s, len) = list_as_string(lst);
@ -116,12 +116,12 @@ vm_obj string_to_list(vm_obj const & s) {
return string_to_list_core(to_vm_string(s).m_value);
}
unsigned string_imp_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
unsigned string_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
data.push_back(string_to_list(o));
return 0;
}
vm_obj string_imp_data(vm_obj const & s) {
vm_obj string_data(vm_obj const & s) {
return string_to_list(s);
}
@ -497,9 +497,9 @@ vm_obj string_hash(vm_obj const & s) {
}
void initialize_vm_string() {
DECLARE_VM_BUILTIN(name({"string_imp", "mk"}), string_imp_mk);
DECLARE_VM_BUILTIN(name({"string_imp", "data"}), string_imp_data);
DECLARE_VM_CASES_BUILTIN(name({"string_imp", "cases_on"}), string_imp_cases_on);
DECLARE_VM_BUILTIN(name({"string", "mk"}), string_mk);
DECLARE_VM_BUILTIN(name({"string", "data"}), string_data);
DECLARE_VM_CASES_BUILTIN(name({"string", "cases_on"}), string_cases_on);
DECLARE_VM_BUILTIN(name({"string", "length"}), string_length);
DECLARE_VM_BUILTIN(name({"string", "empty"}), string_empty);