Library iris.proofmode.spec_patterns

From stdpp Require Export strings.
From iris.proofmode Require Import base tokens.
From iris.prelude Require Import options.

Inductive goal_kind := GSpatial | GModal | GIntuitionistic.

Record spec_goal := SpecGoal {
  spec_goal_kind : goal_kind;
  spec_goal_negate : bool;
  spec_goal_frame : list ident;
  spec_goal_hyps : list ident;
  spec_goal_done : bool
}.

Inductive spec_pat :=
  | SIdent : ident list spec_pat spec_pat
  | SPureGoal (perform_done : bool) : spec_pat
  | SGoal : spec_goal spec_pat
  | SAutoFrame : goal_kind spec_pat.

Definition goal_kind_modal (k : goal_kind) : bool :=
  match k with GModaltrue | _false end.
Definition spec_pat_modal (p : spec_pat) : bool :=
  match p with
  | SGoal ggoal_kind_modal (spec_goal_kind g)
  | SAutoFrame kgoal_kind_modal k
  | _false
  end.

Module spec_pat.
Inductive stack_item :=
  | StPat : spec_pat stack_item
  | StIdent : string stack_item.
Notation stack := (list stack_item).

Fixpoint close (k : stack) (ps : list spec_pat) : option (list spec_pat) :=
  match k with
  | []Some ps
  | StPat p :: kclose k (p :: ps)
  | StIdent _ :: _None
  end.

Fixpoint close_ident (k : stack) (ps : list spec_pat) : option stack :=
  match k with
  | []None
  | StPat p :: kclose_ident k (p :: ps)
  | StIdent s :: kSome (StPat (SIdent s ps) :: k)
  end.

Fixpoint parse_go (ts : list token) (k : stack) : option (list spec_pat) :=
  match ts with
  | []close k []
  | TParenL :: TName s :: tsparse_go ts (StIdent s :: k)
  | TParenR :: tsk close_ident k []; parse_go ts k
  | TName s :: tsparse_go ts (StPat (SIdent s []) :: k)
  | TBracketL :: TIntuitionistic :: TFrame :: TBracketR :: ts
     parse_go ts (StPat (SAutoFrame GIntuitionistic) :: k)
  | TBracketL :: TFrame :: TBracketR :: ts
     parse_go ts (StPat (SAutoFrame GSpatial) :: k)
  | TBracketL :: TModal :: TFrame :: TBracketR :: ts
     parse_go ts (StPat (SAutoFrame GModal) :: k)
  | TBracketL :: TPure None :: TBracketR :: ts
     parse_go ts (StPat (SPureGoal false) :: k)
  | TBracketL :: TPure None :: TDone :: TBracketR :: ts
     parse_go ts (StPat (SPureGoal true) :: k)
  | TBracketL :: TIntuitionistic :: tsparse_goal ts GIntuitionistic false [] [] k
  | TBracketL :: TModal :: tsparse_goal ts GModal false [] [] k
  | TBracketL :: tsparse_goal ts GSpatial false [] [] k
  | _None
  end
with parse_goal (ts : list token)
    (ki : goal_kind) (neg : bool) (frame hyps : list ident)
    (k : stack) : option (list spec_pat) :=
  match ts with
  | TMinus :: ts
     guard (¬neg frame = [] hyps = []);;
     parse_goal ts ki true frame hyps k
  | TName s :: tsparse_goal ts ki neg frame (INamed s :: hyps) k
  | TFrame :: TName s :: tsparse_goal ts ki neg (INamed s :: frame) hyps k
  | TDone :: TBracketR :: ts
     parse_go ts (StPat (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) true)) :: k)
  | TBracketR :: ts
     parse_go ts (StPat (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) false)) :: k)
  | _None
  end.
Definition parse (s : string) : option (list spec_pat) :=
  parse_go (tokenize s) [].

Ltac parse s :=
  lazymatch type of s with
  | list spec_pats
  | spec_patconstr:([s])
  | string
     lazymatch eval vm_compute in (parse s) with
     | Some ?patspats
     | _fail "spec_pat.parse: cannot parse" s "as a specialization pattern"
     end
  | identconstr:([SIdent s []])
  | ?Xfail "spec_pat.parse: the term" s
     "is expected to be a specialization pattern"
     "(usually a string),"
     "but has unexpected type" X
  end.
End spec_pat.