unofficial mirror of emacs-devel@gnu.org 
 help / color / mirror / code / Atom feed
* Documentation on debugging regexp performance
@ 2016-01-21  5:29 Clément Pit--Claudel
  2016-01-21  6:36 ` Yuri Khan
                   ` (2 more replies)
  0 siblings, 3 replies; 13+ messages in thread
From: Clément Pit--Claudel @ 2016-01-21  5:29 UTC (permalink / raw)
  To: Emacs developers


[-- Attachment #1.1: Type: text/plain, Size: 571 bytes --]

Hi emacs-devel,

I'm running into a surprising regular expressions issue. I have attached a file (~50k) in which (re-search-forward "   +[^:=]+ +:=?") seems to be extremely slow. (I killed it after 30 seconds). Truncating the file to its first 20 lines reduces the time for re-search-forward to about a second, which is still extremely slow. 

Are there good resources on how to rewrite regexps to make them Emacs-friendly? I didn't find such documentation, and I'm puzzled as to what could make the regexp above hard to re-search-forward for.

Cheers,
Clément.

[-- Attachment #1.2: large-goal --]
[-- Type: text/plain, Size: 48957 bytes --]

Vector.t methSig (S q0) =>
                                       match
                                         v0 as v'0 in (Vector.t _ m0)
                                         return
                                           (match m0 as m1 return (.. -> ..) with
                                            | O => fun _ : Vector.t methSig O => False -> True
                                            | S n0 => fun _ : Vector.t methSig .. => Fin.t n0 -> methSig
                                            end v'0)
                                       with
                                       | Vector.nil => fun devil : False => match devil return True with
                                                  end
                                       | Vector.cons _ n0 t0 => fun p1 : Fin.t n0 => nth_fix n0 t0 p1
                                       end p'0
                                   end v') n t p0
                            end p'
                        end
                          (VectorDef.cons methSig
                             (Build_methSig
                                (String (Ascii false false true false true true true false)
                                   (String (Ascii true true true true false true true false)
                                      (String (Ascii true true true true true false true false)
                                         (String (Ascii true true false false true true true false)
                                            (String 
                                               (Ascii false false true false true true true false)
                                               (String 
                                                  (Ascii false true false false true true true false)
                                                  (String 
                                                  (Ascii true false false true false true true false)
                                                  (String 
                                                  (Ascii false true true true false true true false)
                                                  (String 
                                                  (Ascii true true true false false true true false) EmptyString)))))))))
                                (@nil Type)
                                (@Some Type
                                   match HSLM return Type with
                                   | Build_StringLikeMin String0 _ _ => String0
                                   end)) (S (S (S (S (S (S O))))))
                             (VectorDef.cons methSig
                                (Build_methSig
                                   (String (Ascii true true false false false true true false)
                                      (String (Ascii false false false true false true true false)
                                         (String (Ascii true false false false false true true false)
                                            (String 
                                               (Ascii false true false false true true true false)
                                               (String 
                                                  (Ascii true true true true true false true false)
                                                  (String 
                                                  (Ascii true false false false false true true false)
                                                  (String 
                                                  (Ascii false false true false true true true false)
                                                  (String 
                                                  (Ascii true true true true true false true false)
                                                  (String 
                                                  (Ascii true false true true false true true false)
                                                  (String (..) (..)))))))))))
                                   (@cons Type nat (@cons Type (ascii -> bool) (@nil Type))) 
                                   (@Some Type bool)) 
                                (S (S (S (S (S O)))))
                                (VectorDef.cons methSig
                                   (Build_methSig
                                      (String (Ascii true true true false false true true false)
                                         (String (Ascii true false true false false true true false)
                                            (String (Ascii false false true false true true true false) EmptyString)))
                                      (@cons Type nat (@nil Type)) 
                                      (@Some Type ascii)) 
                                   (S (S (S (S O))))
                                   (VectorDef.cons methSig
                                      (Build_methSig
                                         (String (Ascii false false true true false true true false)
                                            (String 
                                               (Ascii true false true false false true true false)
                                               (String 
                                                  (Ascii false true true true false true true false)
                                                  (String 
                                                  (Ascii true true true false false true true false)
                                                  (String 
                                                  (Ascii false false true false true true true false)
                                                  (String 
                                                  (Ascii false false false true false true true false) EmptyString))))))
                                         (@nil Type) 
                                         (@Some Type nat)) 
                                      (S (S (S O)))
                                      (VectorDef.cons methSig
                                         (Build_methSig
                                            (String 
                                               (Ascii false false true false true true true false)
                                               (String 
                                                  (Ascii true false false false false true true false)
                                                  (String 
                                                  (Ascii true true false true false true true false)
                                                  (String 
                                                  (Ascii true false true false false true true false) EmptyString))))
                                            (@cons Type nat (@nil Type)) 
                                            (@None Type)) 
                                         (S (S O))
                                         (VectorDef.cons methSig
                                            (Build_methSig
                                               (String 
                                                  (Ascii false false true false false true true false)
                                                  (String 
                                                  (Ascii false true false false true true true false)
                                                  (String 
                                                  (Ascii true true true true false true true false)
                                                  (String 
                                                  (Ascii false false false false true true true false) EmptyString))))
                                               (@cons Type nat (@nil Type)) 
                                               (@None Type)) 
                                            (S O)
                                            (VectorDef.cons methSig
                                               (Build_methSig
                                                  (String 
                                                  (Ascii true true false false true true true false)
                                                  (String 
                                                  (Ascii false false false false true true true false)
                                                  (String 
                                                  (Ascii false false true true false true true false)
                                                  (String 
                                                  (Ascii true false false true false true true false)
                                                  (String (..) (..))))))
                                                  (@cons 
                                                  Type 
                                                  (prod nat (prod nat nat))
                                                  (@cons Type nat (@cons Type nat (@nil Type))))
                                                  (@Some Type (list nat))) O 
                                               (VectorDef.nil methSig)))))))) 
                        return (list Type)
                      with
                      | Build_methSig _ methDom _ => methDom
                      end
                      match
                        match idx in (Fin.t m') return (Vector.t methSig m' -> methSig) with
                        | Fin.F1 q =>
                            fun v : Vector.t methSig (S q) =>
                            match
                              v as v' in (Vector.t _ m)
                              return
                                (match m as m0 return (Vector.t methSig m0 -> Type) with
                                 | O => fun _ : Vector.t methSig O => False -> True
                                 | S n => fun _ : Vector.t methSig (S n) => methSig
                                 end v')
                            with
                            | Vector.nil => fun devil : False => match devil return True with
                                                  end
                            | Vector.cons h n _ => h
                            end
                        | Fin.FS q p' =>
                            fun v : Vector.t methSig (S q) =>
                            match
                              v as v' in (Vector.t _ m)
                              return
                                (match m as m0 return (Vector.t methSig m0 -> Type) with
                                 | O => fun _ : Vector.t methSig O => False -> True
                                 | S n => fun _ : Vector.t methSig (S n) => Fin.t n -> methSig
                                 end v')
                            with
                            | Vector.nil => fun devil : False => match devil return True with
                                                  end
                            | Vector.cons _ n t =>
                                fun p0 : Fin.t n =>
                                (fix nth_fix (m : nat) (v' : Vector.t methSig m) (p : Fin.t m) {struct v'} :
                                   methSig :=
                                   match p in (Fin.t m') return (Vector.t methSig m' -> methSig) with
                                   | Fin.F1 q0 =>
                                       fun v0 : Vector.t methSig (S q0) =>
                                       match
                                         v0 as v'0 in (Vector.t _ m0)
                                         return
                                           (match m0 as m1 return (Vector.t methSig m1 -> Type) with
                                            | O => fun _ : Vector.t methSig O => False -> True
                                            | S n0 => fun _ : Vector.t methSig (..) => methSig
                                            end v'0)
                                       with
                                       | Vector.nil => fun devil : False => match devil return True with
                                                  end
                                       | Vector.cons h n0 _ => h
                                       end
                                   | Fin.FS q0 p'0 =>
                                       fun v0 : Vector.t methSig (S q0) =>
                                       match
                                         v0 as v'0 in (Vector.t _ m0)
                                         return
                                           (match m0 as m1 return (.. -> ..) with
                                            | O => fun _ : Vector.t methSig O => False -> True
                                            | S n0 => fun _ : Vector.t methSig .. => Fin.t n0 -> methSig
                                            end v'0)
                                       with
                                       | Vector.nil => fun devil : False => match devil return True with
                                                  end
                                       | Vector.cons _ n0 t0 => fun p1 : Fin.t n0 => nth_fix n0 t0 p1
                                       end p'0
                                   end v') n t p0
                            end p'
                        end
                          (VectorDef.cons methSig
                             (Build_methSig
                                (String (Ascii false false true false true true true false)
                                   (String (Ascii true true true true false true true false)
                                      (String (Ascii true true true true true false true false)
                                         (String (Ascii true true false false true true true false)
                                            (String 
                                               (Ascii false false true false true true true false)
                                               (String 
                                                  (Ascii false true false false true true true false)
                                                  (String 
                                                  (Ascii true false false true false true true false)
                                                  (String 
                                                  (Ascii false true true true false true true false)
                                                  (String 
                                                  (Ascii true true true false false true true false) EmptyString)))))))))
                                (@nil Type)
                                (@Some Type
                                   match HSLM return Type with
                                   | Build_StringLikeMin String0 _ _ => String0
                                   end)) (S (S (S (S (S (S O))))))
                             (VectorDef.cons methSig
                                (Build_methSig
                                   (String (Ascii true true false false false true true false)
                                      (String (Ascii false false false true false true true false)
                                         (String (Ascii true false false false false true true false)
                                            (String 
                                               (Ascii false true false false true true true false)
                                               (String 
                                                  (Ascii true true true true true false true false)
                                                  (String 
                                                  (Ascii true false false false false true true false)
                                                  (String 
                                                  (Ascii false false true false true true true false)
                                                  (String 
                                                  (Ascii true true true true true false true false)
                                                  (String 
                                                  (Ascii true false true true false true true false)
                                                  (String (..) (..)))))))))))
                                   (@cons Type nat (@cons Type (ascii -> bool) (@nil Type))) 
                                   (@Some Type bool)) 
                                (S (S (S (S (S O)))))
                                (VectorDef.cons methSig
                                   (Build_methSig
                                      (String (Ascii true true true false false true true false)
                                         (String (Ascii true false true false false true true false)
                                            (String (Ascii false false true false true true true false) EmptyString)))
                                      (@cons Type nat (@nil Type)) 
                                      (@Some Type ascii)) 
                                   (S (S (S (S O))))
                                   (VectorDef.cons methSig
                                      (Build_methSig
                                         (String (Ascii false false true true false true true false)
                                            (String 
                                               (Ascii true false true false false true true false)
                                               (String 
                                                  (Ascii false true true true false true true false)
                                                  (String 
                                                  (Ascii true true true false false true true false)
                                                  (String 
                                                  (Ascii false false true false true true true false)
                                                  (String 
                                                  (Ascii false false false true false true true false) EmptyString))))))
                                         (@nil Type) 
                                         (@Some Type nat)) 
                                      (S (S (S O)))
                                      (VectorDef.cons methSig
                                         (Build_methSig
                                            (String 
                                               (Ascii false false true false true true true false)
                                               (String 
                                                  (Ascii true false false false false true true false)
                                                  (String 
                                                  (Ascii true true false true false true true false)
                                                  (String 
                                                  (Ascii true false true false false true true false) EmptyString))))
                                            (@cons Type nat (@nil Type)) 
                                            (@None Type)) 
                                         (S (S O))
                                         (VectorDef.cons methSig
                                            (Build_methSig
                                               (String 
                                                  (Ascii false false true false false true true false)
                                                  (String 
                                                  (Ascii false true false false true true true false)
                                                  (String 
                                                  (Ascii true true true true false true true false)
                                                  (String 
                                                  (Ascii false false false false true true true false) EmptyString))))
                                               (@cons Type nat (@nil Type)) 
                                               (@None Type)) 
                                            (S O)
                                            (VectorDef.cons methSig
                                               (Build_methSig
                                                  (String 
                                                  (Ascii true true false false true true true false)
                                                  (String 
                                                  (Ascii false false false false true true true false)
                                                  (String 
                                                  (Ascii false false true true false true true false)
                                                  (String 
                                                  (Ascii true false false true false true true false)
                                                  (String (..) (..))))))
                                                  (@cons 
                                                  Type 
                                                  (prod nat (prod nat nat))
                                                  (@cons Type nat (@cons Type nat (@nil Type))))
                                                  (@Some Type (list nat))) O 
                                               (VectorDef.nil methSig)))))))) 
                        return (option Type)
                      with
                      | Build_methSig _ _ methCod => methCod
                      end)
                     (@Fin.FS (S (S (S (S (S (S O))))))
                        (@Fin.FS (S (S (S (S (S O)))))
                           (@Fin.FS (S (S (S (S O))))
                              (@Fin.FS (S (S (S O))) (@Fin.FS (S (S O)) (@Fin.FS (S O) (@Fin.F1 O)))))))))
               (@snd (list Type) (option Type)
                  ((fun idx : Fin.t (S (S (S (S (S (S (S O))))))) =>
                    @pair (list Type) (option Type)
                      match
                        match idx in (Fin.t m') return (Vector.t methSig m' -> methSig) with
                        | Fin.F1 q =>
                            fun v : Vector.t methSig (S q) =>
                            match
                              v as v' in (Vector.t _ m)
                              return
                                (match m as m0 return (Vector.t methSig m0 -> Type) with
                                 | O => fun _ : Vector.t methSig O => False -> True
                                 | S n => fun _ : Vector.t methSig (S n) => methSig
                                 end v')
                            with
                            | Vector.nil => fun devil : False => match devil return True with
                                                  end
                            | Vector.cons h n _ => h
                            end
                        | Fin.FS q p' =>
                            fun v : Vector.t methSig (S q) =>
                            match
                              v as v' in (Vector.t _ m)
                              return
                                (match m as m0 return (Vector.t methSig m0 -> Type) with
                                 | O => fun _ : Vector.t methSig O => False -> True
                                 | S n => fun _ : Vector.t methSig (S n) => Fin.t n -> methSig
                                 end v')
                            with
                            | Vector.nil => fun devil : False => match devil return True with
                                                  end
                            | Vector.cons _ n t =>
                                fun p0 : Fin.t n =>
                                (fix nth_fix (m : nat) (v' : Vector.t methSig m) (p : Fin.t m) {struct v'} :
                                   methSig :=
                                   match p in (Fin.t m') return (Vector.t methSig m' -> methSig) with
                                   | Fin.F1 q0 =>
                                       fun v0 : Vector.t methSig (S q0) =>
                                       match
                                         v0 as v'0 in (Vector.t _ m0)
                                         return
                                           (match m0 as m1 return (Vector.t methSig m1 -> Type) with
                                            | O => fun _ : Vector.t methSig O => False -> True
                                            | S n0 => fun _ : Vector.t methSig (..) => methSig
                                            end v'0)
                                       with
                                       | Vector.nil => fun devil : False => match devil return True with
                                                  end
                                       | Vector.cons h n0 _ => h
                                       end
                                   | Fin.FS q0 p'0 =>
                                       fun v0 : Vector.t methSig (S q0) =>
                                       match
                                         v0 as v'0 in (Vector.t _ m0)
                                         return
                                           (match m0 as m1 return (.. -> ..) with
                                            | O => fun _ : Vector.t methSig O => False -> True
                                            | S n0 => fun _ : Vector.t methSig .. => Fin.t n0 -> methSig
                                            end v'0)
                                       with
                                       | Vector.nil => fun devil : False => match devil return True with
                                                  end
                                       | Vector.cons _ n0 t0 => fun p1 : Fin.t n0 => nth_fix n0 t0 p1
                                       end p'0
                                   end v') n t p0
                            end p'
                        end
                          (VectorDef.cons methSig
                             (Build_methSig
                                (String (Ascii false false true false true true true false)
                                   (String (Ascii true true true true false true true false)
                                      (String (Ascii true true true true true false true false)
                                         (String (Ascii true true false false true true true false)
                                            (String 
                                               (Ascii false false true false true true true false)
                                               (String 
                                                  (Ascii false true false false true true true false)
                                                  (String 
                                                  (Ascii true false false true false true true false)
                                                  (String 
                                                  (Ascii false true true true false true true false)
                                                  (String 
                                                  (Ascii true true true false false true true false) EmptyString)))))))))
                                (@nil Type)
                                (@Some Type
                                   match HSLM return Type with
                                   | Build_StringLikeMin String0 _ _ => String0
                                   end)) (S (S (S (S (S (S O))))))
                             (VectorDef.cons methSig
                                (Build_methSig
                                   (String (Ascii true true false false false true true false)
                                      (String (Ascii false false false true false true true false)
                                         (String (Ascii true false false false false true true false)
                                            (String 
                                               (Ascii false true false false true true true false)
                                               (String 
                                                  (Ascii true true true true true false true false)
                                                  (String 
                                                  (Ascii true false false false false true true false)
                                                  (String 
                                                  (Ascii false false true false true true true false)
                                                  (String 
                                                  (Ascii true true true true true false true false)
                                                  (String 
                                                  (Ascii true false true true false true true false)
                                                  (String (..) (..)))))))))))
                                   (@cons Type nat (@cons Type (ascii -> bool) (@nil Type))) 
                                   (@Some Type bool)) 
                                (S (S (S (S (S O)))))
                                (VectorDef.cons methSig
                                   (Build_methSig
                                      (String (Ascii true true true false false true true false)
                                         (String (Ascii true false true false false true true false)
                                            (String (Ascii false false true false true true true false) EmptyString)))
                                      (@cons Type nat (@nil Type)) 
                                      (@Some Type ascii)) 
                                   (S (S (S (S O))))
                                   (VectorDef.cons methSig
                                      (Build_methSig
                                         (String (Ascii false false true true false true true false)
                                            (String 
                                               (Ascii true false true false false true true false)
                                               (String 
                                                  (Ascii false true true true false true true false)
                                                  (String 
                                                  (Ascii true true true false false true true false)
                                                  (String 
                                                  (Ascii false false true false true true true false)
                                                  (String 
                                                  (Ascii false false false true false true true false) EmptyString))))))
                                         (@nil Type) 
                                         (@Some Type nat)) 
                                      (S (S (S O)))
                                      (VectorDef.cons methSig
                                         (Build_methSig
                                            (String 
                                               (Ascii false false true false true true true false)
                                               (String 
                                                  (Ascii true false false false false true true false)
                                                  (String 
                                                  (Ascii true true false true false true true false)
                                                  (String 
                                                  (Ascii true false true false false true true false) EmptyString))))
                                            (@cons Type nat (@nil Type)) 
                                            (@None Type)) 
                                         (S (S O))
                                         (VectorDef.cons methSig
                                            (Build_methSig
                                               (String 
                                                  (Ascii false false true false false true true false)
                                                  (String 
                                                  (Ascii false true false false true true true false)
                                                  (String 
                                                  (Ascii true true true true false true true false)
                                                  (String 
                                                  (Ascii false false false false true true true false) EmptyString))))
                                               (@cons Type nat (@nil Type)) 
                                               (@None Type)) 
                                            (S O)
                                            (VectorDef.cons methSig
                                               (Build_methSig
                                                  (String 
                                                  (Ascii true true false false true true true false)
                                                  (String 
                                                  (Ascii false false false false true true true false)
                                                  (String 
                                                  (Ascii false false true true false true true false)
                                                  (String 
                                                  (Ascii true false false true false true true false)
                                                  (String (..) (..))))))
                                                  (@cons 
                                                  Type 
                                                  (prod nat (prod nat nat))
                                                  (@cons Type nat (@cons Type nat (@nil Type))))
                                                  (@Some Type (list nat))) O 
                                               (VectorDef.nil methSig)))))))) 
                        return (list Type)
                      with
                      | Build_methSig _ methDom _ => methDom
                      end
                      match
                        match idx in (Fin.t m') return (Vector.t methSig m' -> methSig) with
                        | Fin.F1 q =>
                            fun v : Vector.t methSig (S q) =>
                            match
                              v as v' in (Vector.t _ m)
                              return
                                (match m as m0 return (Vector.t methSig m0 -> Type) with
                                 | O => fun _ : Vector.t methSig O => False -> True
                                 | S n => fun _ : Vector.t methSig (S n) => methSig
                                 end v')
                            with
                            | Vector.nil => fun devil : False => match devil return True with
                                                  end
                            | Vector.cons h n _ => h
                            end
                        | Fin.FS q p' =>
                            fun v : Vector.t methSig (S q) =>
                            match
                              v as v' in (Vector.t _ m)
                              return
                                (match m as m0 return (Vector.t methSig m0 -> Type) with
                                 | O => fun _ : Vector.t methSig O => False -> True
                                 | S n => fun _ : Vector.t methSig (S n) => Fin.t n -> methSig
                                 end v')
                            with
                            | Vector.nil => fun devil : False => match devil return True with
                                                  end
                            | Vector.cons _ n t =>
                                fun p0 : Fin.t n =>
                                (fix nth_fix (m : nat) (v' : Vector.t methSig m) (p : Fin.t m) {struct v'} :
                                   methSig :=
                                   match p in (Fin.t m') return (Vector.t methSig m' -> methSig) with
                                   | Fin.F1 q0 =>
                                       fun v0 : Vector.t methSig (S q0) =>
                                       match
                                         v0 as v'0 in (Vector.t _ m0)
                                         return
                                           (match m0 as m1 return (Vector.t methSig m1 -> Type) with
                                            | O => fun _ : Vector.t methSig O => False -> True
                                            | S n0 => fun _ : Vector.t methSig (..) => methSig
                                            end v'0)
                                       with
                                       | Vector.nil => fun devil : False => match devil return True with
                                                  end
                                       | Vector.cons h n0 _ => h
                                       end
                                   | Fin.FS q0 p'0 =>
                                       fun v0 : Vector.t methSig (S q0) =>
                                       match
                                         v0 as v'0 in (Vector.t _ m0)
                                         return
                                           (match m0 as m1 return (.. -> ..) with
                                            | O => fun _ : Vector.t methSig O => False -> True
                                            | S n0 => fun _ : Vector.t methSig .. => Fin.t n0 -> methSig
                                            end v'0)
                                       with
                                       | Vector.nil => fun devil : False => match devil return True with
                                                  end
                                       | Vector.cons _ n0 t0 => fun p1 : Fin.t n0 => nth_fix n0 t0 p1
                                       end p'0
                                   end v') n t p0
                            end p'
                        end
                          (VectorDef.cons methSig
                             (Build_methSig
                                (String (Ascii false false true false true true true false)
                                   (String (Ascii true true true true false true true false)
                                      (String (Ascii true true true true true false true false)
                                         (String (Ascii true true false false true true true false)
                                            (String 
                                               (Ascii false false true false true true true false)
                                               (String 
                                                  (Ascii false true false false true true true false)
                                                  (String 
                                                  (Ascii true false false true false true true false)
                                                  (String 
                                                  (Ascii false true true true false true true false)
                                                  (String 
                                                  (Ascii true true true false false true true false) EmptyString)))))))))
                                (@nil Type)
                                (@Some Type
                                   match HSLM return Type with
                                   | Build_StringLikeMin String0 _ _ => String0
                                   end)) (S (S (S (S (S (S O))))))
                             (VectorDef.cons methSig
                                (Build_methSig
                                   (String (Ascii true true false false false true true false)
                                      (String (Ascii false false false true false true true false)
                                         (String (Ascii true false false false false true true false)
                                            (String 
                                               (Ascii false true false false true true true false)
                                               (String 
                                                  (Ascii true true true true true false true false)
                                                  (String 
                                                  (Ascii true false false false false true true false)
                                                  (String 
                                                  (Ascii false false true false true true true false)
                                                  (String 
                                                  (Ascii true true true true true false true false)
                                                  (String 
                                                  (Ascii true false true true false true true false)
                                                  (String (..) (..)))))))))))
                                   (@cons Type nat (@cons Type (ascii -> bool) (@nil Type))) 
                                   (@Some Type bool)) 
                                (S (S (S (S (S O)))))
                                (VectorDef.cons methSig
                                   (Build_methSig
                                      (String (Ascii true true true false false true true false)
                                         (String (Ascii true false true false false true true false)
                                            (String (Ascii false false true false true true true false) EmptyString)))
                                      (@cons Type nat (@nil Type)) 
                                      (@Some Type ascii)) 
                                   (S (S (S (S O))))
                                   (VectorDef.cons methSig
                                      (Build_methSig
                                         (String (Ascii false false true true false true true false)
                                            (String 
                                               (Ascii true false true false false true true false)
                                               (String 
                                                  (Ascii false true true true false true true false)
                                                  (String 
                                                  (Ascii true true true false false true true false)
                                                  (String 
                                                  (Ascii false false true false true true true false)
                                                  (String 
                                                  (Ascii false false false true false true true false) EmptyString))))))
                                         (@nil Type) 
                                         (@Some Type nat)) 
                                      (S (S (S O)))
                                      (VectorDef.cons methSig
                                         (Build_methSig
                                            (String 
                                               (Ascii false false true false true true true false)
                                               (String 
                                                  (Ascii true false false false false true true false)
                                                  (String 
                                                  (Ascii true true false true false true true false)
                                                  (String 
                                                  (Ascii true false true false false true true false) EmptyString))))
                                            (@cons Type nat (@nil Type)) 
                                            (@None Type)) 
                                         (S (S O))
                                         (VectorDef.cons methSig
                                            (Build_methSig
                                               (String 
                                                  (Ascii false false true false false true true false)
                                                  (String 
                                                  (Ascii false true false false true true true false)
                                                  (String 
                                                  (Ascii true true true true false true true false)
                                                  (String 
                                                  (Ascii false false false false true true true false) EmptyString))))
                                               (@cons Type nat (@nil Type)) 
                                               (@None Type)) 
                                            (S O)
                                            (VectorDef.cons methSig
                                               (Build_methSig
                                                  (String 
                                                  (Ascii true true false false true true true false)
                                                  (String 
                                                  (Ascii false false false false true true true false)
                                                  (String 
                                                  (Ascii false false true true false true true false)
                                                  (String 
                                                  (Ascii true false false true false true true false)
                                                  (String (..) (..))))))
                                                  (@cons 
                                                  Type 
                                                  (prod nat (prod nat nat))
                                                  (@cons Type nat (@cons Type nat (@nil Type))))
                                                  (@Some Type (list nat))) O 
                                               (VectorDef.nil methSig)))))))) 
                        return (option Type)
                      with
                      | Build_methSig _ _ methCod => methCod
                      end)
                     (@Fin.FS (S (S (S (S (S (S O))))))
                        (@Fin.FS (S (S (S (S (S O)))))
                           (@Fin.FS (S (S (S (S O))))
                              (@Fin.FS (S (S (S O))) (@Fin.FS (S (S O)) (@Fin.FS (S O) (@Fin.F1 O)))))))))))
         (methCod
            (Build_methSig
               (String (Ascii true true false false true true true false)
                  (String (Ascii false false false false true true true false)
                     (String (Ascii false false true true false true true false)
                        (String (Ascii true false false true false true true false)
                           (String (Ascii false false true false true true true false)
                              (String (Ascii true true false false true true true false) EmptyString))))))
               (@fst (list Type) (option Type)
                  ((fun idx : Fin.t (S (S (S (S (S (S (S O))))))) =>
                    @pair (list Type) (option Type)
                      match
                        match idx in (Fin.t m') return (Vector.t methSig m' -> methSig) with
                        | Fin.F1 q =>
                            fun v : Vector.t methSig (S q) =>
                            match
                              v as v' in (Vector.t _ m)
                              return
                                (match m as m0 return (Vector.t methSig m0 -> Type) with
                                 | O => fun _ : Vector.t methSig O => False -> True
                                 | S n => fun _ : Vector.t methSig (S n) => methSig
                                 end v')
                            with
                            | Vector.nil => fun devil : False => match devil return True with
                                                  end
                            | Vector.cons h n _ => h
                            end
                        | Fin.FS q p' =>

[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]

^ permalink raw reply	[flat|nested] 13+ messages in thread

end of thread, other threads:[~2016-01-23  6:12 UTC | newest]

Thread overview: 13+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2016-01-21  5:29 Documentation on debugging regexp performance Clément Pit--Claudel
2016-01-21  6:36 ` Yuri Khan
2016-01-21  9:39   ` Alexis
2016-01-21 13:22     ` Clément Pit--Claudel
2016-01-21 22:10     ` Marcin Borkowski
2016-01-22  7:02       ` Alexis
2016-01-22 14:32       ` Clément Pit--Claudel
2016-01-21 11:42 ` Wolfgang Jenkner
2016-01-21 16:38   ` Clément Pit--Claudel
2016-01-21 15:27 ` Alan Mackenzie
2016-01-21 16:37   ` Clément Pit--Claudel
2016-01-21 17:16     ` Alan Mackenzie
2016-01-23  6:12       ` Stefan Monnier

Code repositories for project(s) associated with this public inbox

	https://git.savannah.gnu.org/cgit/emacs.git

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).