Quelle  g_redexpr.mlg   Sprache: unbekannt

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

DECLARE GLOBAL PLUGIN

{
open Procq
open Procq.Prim
open Procq.Constr
open Pvernac.Vernac_

open Util
open Locus
open Genredexpr

let all_with ~head delta =
  let all = [FBeta;FMatch;FFix;FCofix;FZeta;delta] in
  Redops.make_red_flag (if head then FHead :: all else all)

let int_or_var = Entry.make "int_or_var"
let nat_or_var = Entry.make "nat_or_var"
let pattern_occ = Entry.make "pattern_occ"
let unfold_occ = Entry.make "unfold_occ"
let ref_or_pattern_occ = Entry.make "ref_or_pattern_occ"
let occs_nums = Entry.make "occs_nums"
let occs = Entry.make "occs"
let delta_flag = Entry.make "delta_flag"
let strategy_flag = Entry.make "strategy_flag"
}


GRAMMAR EXTEND Gram
  GLOBAL: int_or_var nat_or_var occs occs_nums unfold_occ pattern_occ
    delta_flag strategy_flag ref_or_pattern_occ red_expr;

  int_or_var:
    [ [ n = integer  -> { ArgArg n }
      | id = identref -> { ArgVar id } ] ]
  ;
  nat_or_var:
    [ [ n = natural  -> { ArgArg n }
      | id = identref -> { ArgVar id } ] ]
  ;

  occs_nums:
    [ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl }
      | "-"; nl = LIST1 nat_or_var -> { AllOccurrencesBut nl } ] ]
  ;
  occs:
    [ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ]
  ;
  pattern_occ:
    [ [ c = constr; nl = occs -> { (nl,c) } ] ]
  ;
  ref_or_pattern_occ:
    (* If a string, it is interpreted as a ref
       (anyway a Rocq string does not reduce) *)
    [ [ c = smart_global; nl = occs -> { nl,Inl c }
      | c = constr; nl = occs -> { nl,Inr c } ] ]
  ;
  unfold_occ:
    [ [ c = smart_global; nl = occs -> { (nl,c) } ] ]
  ;
  red_flag:
    [ [ IDENT "beta" -> { [FBeta] }
      | IDENT "iota" -> { [FMatch;FFix;FCofix] }
      | IDENT "match" -> { [FMatch] }
      | IDENT "fix" -> { [FFix] }
      | IDENT "cofix" -> { [FCofix] }
      | IDENT "zeta" -> { [FZeta] }
      | IDENT "delta"; d = delta_flag -> { [d] }
      | IDENT "head" -> { [FHead] }
    ] ]
  ;
  delta_flag:
    [ [ "-"; "["; idl = LIST1 smart_global; "]" -> { FDeltaBut idl }
      | "["; idl = LIST1 smart_global; "]" -> { FConst idl }
      | -> { FDeltaBut [] }
    ] ]
  ;
  strategy_flag:
    [ [ s = LIST1 red_flag -> { Redops.make_red_flag (List.flatten s) }
      | h = OPT [ IDENT "head" -> { () } ]; d = delta_flag -> { all_with ~head:(Option.has_some h) d }
    ] ]
  ;

  red_expr:
    [ [ IDENT "red" -> { Red }
      | IDENT "hnf" -> { Hnf }
      | IDENT "simpl"; h = OPT [ IDENT "head" -> { () } ];
        d = delta_flag; po = OPT ref_or_pattern_occ -> { Simpl (all_with ~head:(Option.has_some h) d,po) }
      | IDENT "cbv"; s = strategy_flag -> { Cbv s }
      | IDENT "cbn"; s = strategy_flag -> { Cbn s }
      | IDENT "lazy"; s = strategy_flag -> { Lazy s }
      | IDENT "compute"; delta = delta_flag -> { Cbv (all_with ~head:false delta) }
      | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> { CbvVm po }
      | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> { CbvNative po }
      | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> { Unfold ul }
      | IDENT "fold"; cl = LIST1 constr -> { Fold cl }
      | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> { Pattern pl }
      | s = IDENT -> { ExtraRedExpr s } ] ]
  ;
END