Semantics: remove canonicalize case insenst. property in Params

Engine/Prefix.v

@@ -621,7 +621,7 @@ Proof.
     repeat rewrite Character.numeric_pseudo_bij in H4.
     assumption.
   } subst.
-  repeat rewrite (canonicalize_casesenst rer _ no_i_flag) in H2.
+  repeat rewrite (Character.canonicalize_casesenst rer _ no_i_flag) in H2.
   symmetry. apply EqDec.inversion_true. assumption.
 Qed.
 
@@ -778,15 +778,15 @@ Proof.
   intros rest s c cd no_i_flag Hstart Hmatch.
 
   Ltac unfold_match H no_i_flag :=
-    unfold char_match in H; rewrite (canonicalize_casesenst _ _ no_i_flag) in H.
+    unfold char_match in H; rewrite (Character.canonicalize_casesenst _ _ no_i_flag) in H.
 
   induction cd;
     (* there is no known literal *)
     try solve[simpl; destruct rest; constructor].
   (* CdSingle *)
   - unfold_match Hmatch no_i_flag.
     assert (c = c0). {
-      simpl in Hmatch. rewrite (canonicalize_casesenst _ _ no_i_flag) in Hmatch.
+      simpl in Hmatch. rewrite (Character.canonicalize_casesenst _ _ no_i_flag) in Hmatch.
       eqdec. reflexivity.
     } subst.
     simpl.
@@ -802,12 +802,12 @@ Proof.
     + etransitivity.
       * eapply starts_with_chain_merge_literals.
         intro. eapply extract_literal_char_impossible_no_match; eauto.
-      * eapply IHcd1. unfold char_match. rewrite canonicalize_casesenst; eauto.
+      * eapply IHcd1. unfold char_match. rewrite Character.canonicalize_casesenst; eauto.
     + simpl. rewrite merge_literals_comm.
       etransitivity.
       * eapply starts_with_chain_merge_literals.
         intro. eapply extract_literal_char_impossible_no_match; eauto.
-      * eapply IHcd2. unfold char_match. rewrite canonicalize_casesenst; eauto.
+      * eapply IHcd2. unfold char_match. rewrite Character.canonicalize_casesenst; eauto.
 Qed.
 
 (* generalization of extract_literal_prefix on the group map and the list of actions *)

Rewriting/Anchors.v

@@ -151,6 +151,6 @@ Section Anchors.
     Anchor a ≅[rer] desugar_anchor a.
   Proof.
     intros Hic; apply desugar_anchor_correct.
-    all: intros c; try rewrite canonicalize_casesenst; intuition.
+    all: intros c; try rewrite Character.canonicalize_casesenst; intuition.
   Qed.
 End Anchors.

Semantics/Chars.v

@@ -82,15 +82,15 @@ Section Chars.
   Proof.
     intro Hcasesenst.
     induction l; simpl; auto.
-    rewrite canonicalize_casesenst, IHl by auto. auto.
+    rewrite Character.canonicalize_casesenst, IHl by auto. auto.
   Qed.
 
   Lemma inb_canonicalized_casesenst:
     RegExpRecord.ignoreCase rer = false ->
     forall c l, inb_canonicalized c l = inb c l.
   Proof.
     intros Hcasesenst c l. unfold inb_canonicalized.
-    rewrite canonicalize_casesenst by assumption.
+    rewrite Character.canonicalize_casesenst by assumption.
     rewrite map_canonicalize_casesenst by assumption.
     reflexivity.
   Qed.

Semantics/Inst.v

@@ -7,12 +7,5 @@ using a naive instantiation of Warblre typeclasses *)
 
 Instance character_class: Character.class := @Parameters.character_class parameters.
 
-Lemma canonicalize_casesenst: forall rer chr, RegExpRecord.ignoreCase rer = false -> Character.canonicalize rer chr = chr.
-Proof.
-  intros rer chr Hcasesenst.
-  unfold Character.canonicalize, character_class, Parameters.character_class, parameters, NaiveEngineParameters.Character.canonicalize.
-  rewrite Hcasesenst. reflexivity.
-Qed.
-
 Instance naive_params: LindenParameters :=
-  lindenParameters_of_warblre parameters canonicalize_casesenst.
+  lindenParameters_of_warblre parameters.

Semantics/Parameters.v

@@ -8,21 +8,15 @@ Class LindenParameters := make {
   #[global] char:: Character.class; (* a type of characters, *)
   #[global] unicodeProp:: Parameters.Property.class (@Parameters.Character char); (* a type of Unicode properties, *)
   #[global] charset_class:: @CharSet.class char; (* and a type of character sets. *)
-
-  (* As per the ECMA specification (22.2.2.7.3 Canonicalize ( rer, ch )), when we do not ignore case, canonicalization is the identity function. *)
-  canonicalize_casesenst: forall rer chr, RegExpRecord.ignoreCase rer = false -> Character.canonicalize rer chr = chr;
 }.
 
 Section OfWarblre.
   Context (p: Parameters).
-  Context (canon: forall rer chr,
-              RegExpRecord.ignoreCase rer = false ->
-              Character.canonicalize rer chr = chr).
 
   Definition lindenParameters_of_warblre : LindenParameters :=
     make
       (@Parameters.character_class p)
       (@Parameters.unicode_property_class p)
-      (@Parameters.set_class p)
-      canon.
+      (@Parameters.set_class p).
+
 End OfWarblre.

linden.opam

@@ -30,5 +30,5 @@ build: [
 ]
 x-maintenance-intent: ["(latest)"]
 pin-depends: [
-  ["warblre.0.1.0" "git+https://github.com/LindenRegex/Warblre.git#cb2dab9d197a22e4284497200682793b97bf4121"]
+  ["warblre.0.1.0" "git+https://github.com/LindenRegex/Warblre.git#4321379b887d590a42759818f6d9b1fd2351688e"]
 ]

linden.opam.template

@@ -1,3 +1,3 @@
 pin-depends: [
-  ["warblre.0.1.0" "git+https://github.com/LindenRegex/Warblre.git#cb2dab9d197a22e4284497200682793b97bf4121"]
+  ["warblre.0.1.0" "git+https://github.com/LindenRegex/Warblre.git#4321379b887d590a42759818f6d9b1fd2351688e"]
 ]