lambdapi icon indicating copy to clipboard operation
lambdapi copied to clipboard

Update to pratter 5

Open gabrielhdt opened this issue 10 months ago • 7 comments

From pratter 4, it's possible to interpret a single token in different ways. This allows for instance to consider the symbol - as both the unary and binary minus.

gabrielhdt avatar Feb 12 '25 09:02 gabrielhdt

Is the bumping of the minimal OCaml version really required here? Perhaps this is now not necessary anymore after our monad omission ...? :)

01mf02 avatar Feb 14 '25 18:02 01mf02

I'm afraid the version 4.14 is required by the operation Seq.uncons, monads aren't guilty there

gabrielhdt avatar Feb 17 '25 12:02 gabrielhdt

I guess you could then very easily replace Seq.uncons by something equivalent in Pratter. It's currently used only here:

let tok : ('tok, 'tok option) parser =
 fun inp ->
  match Seq.uncons inp with
  | None -> Ok (None, Seq.empty)
  | Some (t, rest) -> Ok (Some t, rest)

Unfolding Seq.uncons, this could easily be something like (modulo importing Nil and Cons):

let tok : ('tok, 'tok option) parser =
 fun inp ->
  match inp () with
  | Nil -> Ok (None, Seq.empty)
  | Cons (t, rest) -> Ok (Some t, rest)

Not tested, but if uncons is the only reason for bumping the MSOV (minimal supported OCaml version), it might be worth to reconsider that. ;)

01mf02 avatar Feb 19 '25 07:02 01mf02

Hi @gabrielhdt . Michael's suggestion looks nice and easy to implement. Do you want to try it? I will then wait for the version 5.1 of pratter and an update of this PR.

fblanqui avatar Feb 19 '25 10:02 fblanqui

Looks good to me ! I'll give it a shot.

gabrielhdt avatar Feb 21 '25 10:02 gabrielhdt

FYI I've managed to reduced the minimal supported ocaml version to 4.10.

On the question of whether this version is low enough or not, I tend to think that if a program is compatible with Debian stable, it's ok.

Now I just have to publish all that to opam :)

gabrielhdt avatar Mar 06 '25 14:03 gabrielhdt

Hi @gabrielhdt . I see that pratter 5.0.1 is now available on opam. Could you please update your PR so that I can merge it?

fblanqui avatar Apr 30 '25 10:04 fblanqui