Commit 157e41c2 authored by Robbert Krebbers's avatar Robbert Krebbers

Use fast_string.

parent 2cbcc992
......@@ -83,7 +83,6 @@ theories/tests/barrier_client.v
theories/tests/list_reverse.v
theories/tests/tree_sum.v
theories/tests/ipm_paper.v
theories/proofmode/strings.v
theories/proofmode/tokens.v
theories/proofmode/coq_tactics.v
theories/proofmode/environments.v
......
From iris.program_logic Require Export ectx_language ectxi_language.
From iris.algebra Require Export ofe.
From stdpp Require Export strings.
From fast_string Require Export fast_string_lib.
From stdpp Require Import gmap.
Set Default Proof Using "Type".
......
From iris.base_logic Require Export base_logic.
From iris.base_logic Require Import big_op tactics.
From iris.proofmode Require Export environments classes.
From stdpp Require Import stringmap hlist.
Set Default Proof Using "Type".
Import uPred.
Import env_notations.
......@@ -215,11 +214,11 @@ Proof.
apply wand_intro_l; destruct p; simpl.
- apply sep_intro_True_l; [apply pure_intro|].
+ destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
intros j; destruct (strings.string_beq_reflect j i); naive_solver.
intros j; destruct (string_beq_reflect j i); naive_solver.
+ by rewrite always_sep assoc.
- apply sep_intro_True_l; [apply pure_intro|].
+ destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
intros j; destruct (strings.string_beq_reflect j i); naive_solver.
intros j; destruct (string_beq_reflect j i); naive_solver.
+ solve_sep_entails.
Qed.
......
From stdpp Require Export strings.
From iris.proofmode Require Import strings.
From fast_string Require Export fast_string_lib.
From iris.algebra Require Export base.
From stdpp Require Import stringmap.
Set Default Proof Using "Type".
Inductive env (A : Type) : Type :=
......
From stdpp Require Export strings.
From fast_string Require Export fast_string_lib.
From iris.proofmode Require Import tokens.
Set Default Proof Using "Type".
......@@ -70,7 +70,7 @@ Fixpoint close_conj_list (k : stack)
Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
match ts with
| [] => Some k
| TName "_" :: ts => parse_go ts (SPat IDrop :: k)
| TName (String ["_"%char]) :: ts => parse_go ts (SPat IDrop :: k)
| TName s :: ts => parse_go ts (SPat (IName s) :: k)
| TAnom :: ts => parse_go ts (SPat IAnom :: k)
| TFrame :: ts => parse_go ts (SPat IFrame :: k)
......
From iris.proofmode Require Import coq_tactics environments.
From stdpp Require Export strings.
From fast_string Require Export fast_string_lib.
Set Default Proof Using "Type".
Delimit Scope proof_scope with env.
......
From stdpp Require Export strings.
From fast_string Require Export fast_string_lib.
From iris.proofmode Require Import tokens.
Set Default Proof Using "Type".
......
From stdpp Require Export strings.
From fast_string Require Export fast_string_lib.
From iris.proofmode Require Import tokens.
Set Default Proof Using "Type".
......
From stdpp Require Import strings.
From iris.algebra Require Import base.
From Coq Require Import Ascii.
Set Default Proof Using "Type".
Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
Lemma lazy_andb_true (b1 b2 : bool) : b1 && b2 = true b1 = true b2 = true.
Proof. destruct b1, b2; intuition congruence. Qed.
Definition beq (b1 b2 : bool) : bool :=
match b1, b2 with
| false, false | true, true => true
| _, _ => false
end.
Definition ascii_beq (x y : ascii) : bool :=
let 'Ascii x1 x2 x3 x4 x5 x6 x7 x8 := x in
let 'Ascii y1 y2 y3 y4 y5 y6 y7 y8 := y in
beq x1 y1 && beq x2 y2 && beq x3 y3 && beq x4 y4 &&
beq x5 y5 && beq x6 y6 && beq x7 y7 && beq x8 y8.
Fixpoint string_beq (s1 s2 : string) : bool :=
match s1, s2 with
| "", "" => true
| String a1 s1, String a2 s2 => ascii_beq a1 a2 && string_beq s1 s2
| _, _ => false
end.
Lemma beq_true b1 b2 : beq b1 b2 = true b1 = b2.
Proof. destruct b1, b2; simpl; intuition congruence. Qed.
Lemma ascii_beq_true x y : ascii_beq x y = true x = y.
Proof.
destruct x, y; rewrite /= !lazy_andb_true !beq_true. intuition congruence.
Qed.
Lemma string_beq_true s1 s2 : string_beq s1 s2 = true s1 = s2.
Proof.
revert s2. induction s1 as [|x s1 IH]=> -[|y s2] //=.
rewrite lazy_andb_true ascii_beq_true IH. intuition congruence.
Qed.
Lemma string_beq_reflect s1 s2 : reflect (s1 = s2) (string_beq s1 s2).
Proof. apply iff_reflect. by rewrite string_beq_true. Qed.
......@@ -3,12 +3,11 @@ From iris.proofmode Require Import intro_patterns spec_patterns sel_patterns.
From iris.base_logic Require Export base_logic.
From iris.proofmode Require Export classes notation.
From iris.proofmode Require Import class_instances.
From stdpp Require Import stringmap hlist.
From iris.proofmode Require Import strings.
From stdpp Require Import hlist.
Set Default Proof Using "Type".
Declare Reduction env_cbv := cbv [
beq ascii_beq string_beq
char_beq char_list_beq string_beq
env_lookup env_lookup_delete env_delete env_app env_replace env_dom
env_persistent env_spatial env_spatial_is_nil envs_dom
envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
......
From stdpp Require Export strings.
From fast_string Require Export fast_string_lib.
Set Default Proof Using "Type".
Inductive token :=
......@@ -25,39 +25,38 @@ Inductive token :=
| TMinus : token
| TSep : token.
Fixpoint cons_name (kn : string) (k : list token) : list token :=
match kn with "" => k | _ => TName (string_rev kn) :: k end.
Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
Fixpoint cons_name (kn : list char) (k : list token) : list token :=
match kn with [] => k | _ => TName (String (reverse kn)) :: k end.
Fixpoint tokenize_go (s : list char) (k : list token) (kn : list char) : list token :=
match s with
| "" => reverse (cons_name kn k)
| String "?" s => tokenize_go s (TAnom :: cons_name kn k) ""
| String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
| String "[" s => tokenize_go s (TBracketL :: cons_name kn k) ""
| String "]" s => tokenize_go s (TBracketR :: cons_name kn k) ""
| String "|" s => tokenize_go s (TBar :: cons_name kn k) ""
| String "(" s => tokenize_go s (TParenL :: cons_name kn k) ""
| String ")" s => tokenize_go s (TParenR :: cons_name kn k) ""
| String "&" s => tokenize_go s (TAmp :: cons_name kn k) ""
| String "{" s => tokenize_go s (TBraceL :: cons_name kn k) ""
| String "}" s => tokenize_go s (TBraceR :: cons_name kn k) ""
| String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
| String "#" s => tokenize_go s (TAlways :: cons_name kn k) ""
| String ">" s => tokenize_go s (TModal :: cons_name kn k) ""
| String "!" (String "%" s) => tokenize_go s (TPureIntro :: cons_name kn k) ""
| String "!" (String "#" s) => tokenize_go s (TAlwaysIntro :: cons_name kn k) ""
| String "!" (String ">" s) => tokenize_go s (TModalIntro :: cons_name kn k) ""
| String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_name kn k) ""
| String "*" (String "*" s) => tokenize_go s (TAll :: cons_name kn k) ""
| String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
| String "-" s => tokenize_go s (TMinus :: cons_name kn k) ""
| String (Ascii.Ascii false true false false false true true true) (* unicode ∗ *)
(String (Ascii.Ascii false false false true false false false true)
(String (Ascii.Ascii true true true false true false false true) s)) =>
tokenize_go s (TSep :: cons_name kn k) ""
| String a s =>
if is_space a then tokenize_go s (cons_name kn k) ""
else tokenize_go s k (String a kn)
| [] => reverse (cons_name kn k)
| "?" :: s => tokenize_go s (TAnom :: cons_name kn k) []
| "$" :: s => tokenize_go s (TFrame :: cons_name kn k) []
| "[" :: s => tokenize_go s (TBracketL :: cons_name kn k) []
| "]" :: s => tokenize_go s (TBracketR :: cons_name kn k) []
| "|" :: s => tokenize_go s (TBar :: cons_name kn k) []
| "(" :: s => tokenize_go s (TParenL :: cons_name kn k) []
| ")" :: s => tokenize_go s (TParenR :: cons_name kn k) []
| "&" :: s => tokenize_go s (TAmp :: cons_name kn k) []
| "{" :: s => tokenize_go s (TBraceL :: cons_name kn k) []
| "}" :: s => tokenize_go s (TBraceR :: cons_name kn k) []
| "%" :: s => tokenize_go s (TPure :: cons_name kn k) []
| "#" :: s => tokenize_go s (TAlways :: cons_name kn k) []
| ">" :: s => tokenize_go s (TModal :: cons_name kn k) []
| "!" :: "%" :: s => tokenize_go s (TPureIntro :: cons_name kn k) []
| "!" :: "#" :: s => tokenize_go s (TAlwaysIntro :: cons_name kn k) []
| "!" :: ">" :: s => tokenize_go s (TModalIntro :: cons_name kn k) []
| "/" :: "=" :: s => tokenize_go s (TSimpl :: cons_name kn k) []
| "*" :: "*" :: s => tokenize_go s (TAll :: cons_name kn k) []
| "*" :: s => tokenize_go s (TForall :: cons_name kn k) []
| "-" :: s => tokenize_go s (TMinus :: cons_name kn k) []
| C226 :: C136 :: C151 :: s (* unicode ∗ *) =>
tokenize_go s (TSep :: cons_name kn k) []
| a :: s =>
if is_space a then tokenize_go s (cons_name kn k) []
else tokenize_go s k (a :: kn)
(* TODO: Complain about invalid characters, to future-proof this
against making more characters special. *)
end.
Definition tokenize (s : string) : list token := tokenize_go s [] "".
end%char.
Definition tokenize (s : string) : list token :=
tokenize_go (string_car s) [] [].
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment