share/bash/why3

   1 # bash completion for Why3
   2
   3 # To use this script you should have bash-completion package installed
   4 # Put it in /etc/bash_completion.d or just source it from your .bashrc
   5
   6 _why3()
   7 {
   8     local cur prev words cword split
   9
  10     if declare -F _init_completion > /dev/null ; then
  11         _init_completion -s || return
  12     else
  13         _get_comp_words_by_ref -n = cur prev words cword
  14     fi
  15
  16     case "$prev" in
  17         -T|--theory)
  18             # this only completes the first '-T' option
  19             # also, we cannot complete library theories
  20             ${split:-false} || cword=$((cword-1))
  21             words=("${words[@]:0:$cword}" --print-namespace)
  22             theories=$(${words[@]} 2>/dev/null | sed -n -e 's/^\([^ ][^-]*\).*/\1/p')
  23             COMPREPLY=( $( compgen -W "$theories" -- "$cur" ) )
  24             return 0
  25             ;;
  26         -G|--goal)
  27             ${split:-false} || cword=$((cword-1))
  28             words=("${words[@]:0:$cword}" --print-namespace)
  29             goals=$(${words[@]} 2>/dev/null | sed -n -e 's/.*-goal //p')
  30             COMPREPLY=( $( compgen -W "$goals" -- "$cur" ) )
  31             return 0
  32             ;;
  33         -C|--config|--extra-config)
  34             _filedir
  35             return 0
  36             ;;
  37         -L|--library|-I)
  38             _filedir -d
  39             return 0
  40             ;;
  41         -P|--prover)
  42             provers=$($1 config list-provers | sed -n -e 's/^\([^ ]\+\).*/\1/p' | uniq)
  43             COMPREPLY=( $( compgen -W "$provers" -- "$cur" ) )
  44             return 0
  45             ;;
  46         -F|--format)
  47             formats=$($1 show formats | sed -n -e 's/^\([^ ]\+\).*/\1/p')
  48             COMPREPLY=( $( compgen -W "$formats" -- "$cur" ) )
  49             return 0
  50             ;;
  51         -t|--timelimit|-m|--memlimit)
  52             return 0
  53             ;;
  54         -a|--apply-transform)
  55             transforms=$($1 show transformations | grep -e '^  [^ ]')
  56             COMPREPLY=( $( compgen -W "$transforms" -- "$cur" ) )
  57             return 0
  58             ;;
  59         -M|--meta)
  60             metas=$($1 show metas |
  61                 grep -e '^[^ ]\+\( (flag)\)\?\( \[string\]\)\?$' |
  62                 sed -e 's/ (flag)//;s/ \[string\]/=/')
  63             COMPREPLY=( $( compgen -W "$metas" -- "$cur") )
  64             return 0
  65             ;;
  66         -D|--driver)
  67             _filedir
  68             return 0
  69             ;;
  70         -o|--output)
  71             _filedir -d
  72             return 0
  73             ;;
  74         --install-plugin)
  75             _filedir
  76             return 0
  77             ;;
  78         add-prover)
  79             ids=$($1 config list-supported-provers)
  80             COMPREPLY=( $( compgen -W "$ids" -- "$cur") )
  81             return 0
  82             ;;
  83         --smoke-detector)
  84             COMPREPLY=( $( compgen -W 'none top deep' -- "$cur" ) )
  85             return 0
  86             ;;
  87         --debug)
  88             flags=$($1 --list-debug-flags | sed -n -e 's/^\([^ ]\+\).*/\1/p')
  89             COMPREPLY=( $( compgen -W "$flags" -- "$cur" ) )
  90             return 0
  91             ;;
  92         --filter-prover)
  93             provers=$($1 config list-provers | sed -n -e 's/^\([^ ]\+\).*/\1/p' | uniq)
  94             COMPREPLY=( $( compgen -W "$provers" -- "$cur" ) )
  95             return 0
  96             ;;
  97         --filter-obsolete|--filter-archived|--filter-verified-goal|--filter-verified)
  98             COMPREPLY=( $( compgen -W 'yes no all' -- "$cur" ) )
  99             return 0
 100             ;;
 101         --style)
 102             COMPREPLY=( $( compgen -W 'simpletree table' -- "$cur" ) )
 103             return 0
 104             ;;
 105         config|session|show)
 106             cmds=$($1 $prev --help | sed -n -e 's/^  \([^ ]\+\).*/\1/p')
 107             COMPREPLY=( $( compgen -W "$cmds --help -h" -- "$cur" ) )
 108             return 0
 109             ;;
 110     esac
 111
 112     case "$cur" in
 113         -*) words[cword]="--help"
 114             opts=$(_parse_help "${words[@]}")
 115             COMPREPLY=( $( compgen -W "$opts" -- "$cur" ) )
 116             [[ $COMPREPLY == *= ]] && compopt -o nospace
 117             return 0
 118             ;;
 119     esac
 120
 121     if [ $cword -eq 1 ] ; then
 122         cmds=$($1 --help 2>&1 | sed -n -e 's/^  \([a-z]\+\).*/\1/p')
 123         COMPREPLY=( $( compgen -W "$cmds" -- "$cur" ) )
 124         return 0
 125     fi
 126
 127     _filedir
 128
 129 } && complete -F _why3 why3 why3.opt why3.byte