FStar Parsec

parser.fst

module Main

open FStar.Pervasives.Native

type vec a : nat -> Type =
  | NilV : vec a 0
  | ConsV : #n:nat -> hd:a -> tl:vec a n -> vec a (n + 1)

type response a s =
  | Ok   : bool -> a -> s -> response a s
  | Fail : bool      -> s -> response a s

let fold =
  function
  | Ok b a l -> fun o _ -> o b a l
  | Fail b l -> fun _ f -> f b l

(* Parser corner *)

type parser s a (n:nat) (m:nat{m <= n}) = vec s n -> response a (vec s m)

let return #s #a (#n:nat) : a -> parser s a n n = Ok false 

let fail #s #a (#n: nat) : parser s a n n = Fail false 

let any #s (#n: nat) (#m: nat{n = m + 1}): parser s s n m =
    function
    | ConsV a l -> Ok true a l
    | _         -> Fail false NilV

let eos #s (#n: nat) : parser s unit n n = 
    function
    | NilV -> Ok false () NilV
    | l    -> Fail false l

let ( <$> ) #s #a #b (#n: nat) (#m: nat{m <= n}) : parser s a n m -> (a -> b) -> parser s b n m = fun p f -> fun l ->
    match p l with
    | Ok b a l -> Ok b (f a) l
    | Fail b l -> Fail b l
  
(* Type checker fails since l can be a `vec s r` or `vec s m` *)
let ( >>= ) #s #a #b (#n: nat) (#m: nat{m <= n}) (#r: nat{r <= m}) (#t:nat{t = m \/ t = r}) : parser s a n m -> (a -> parser s b m r) -> parser s b n t = fun p f -> fun l ->
    match p l with
    | Ok b a l -> f a l      (* l : vec s r *)
    | Fail b l -> Fail b l   (* l : vec s m *)
(*
let ( <&> ) #s #a #b : parser s a -> parser s b -> parser s (a*b) = fun p1 p2 -> fun l ->
    match p1 l with
    | Fail b1 l -> Fail b1 l
    | Ok b1 a l -> match p2 l with
                   | Ok b2 b l -> Ok (b1 && b2) (a,b) l
                   | Fail b2 l -> Fail b2 l
    
let ( <|> ) #s #a : parser s a -> parser s a -> parser s a = fun p1 p2 -> fun l ->
    match p1 l with
    | Ok b1 a l -> Ok b1 a l
    | Fail b1 l -> match p2 l with
                   | Ok b2 b l -> if b1 then Fail b1 l else Ok b2 b l                 
                   | Fail b2 l -> Fail b2 l

let filter #s : (s -> bool) -> parser s s = fun p l ->
    match l with
    | a :: l -> if p a then (Ok true a l) else (Fail false l)
    | _ -> Fail false l
*)

    

https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/parsec-paper-letter.pdf