print-namespace : print the kind of the lemmas

completion : complete theories and goals

share/zsh/_why3

-#compdef why3
+#compdef whyml3 why3
 ##
 ## zsh completion for why3
 ## generated by ocompl
@@ -8,8 +8,11 @@
 ##
 ##
 
-local curcontext state line cmds ret=1
-local last_file
+typeset -A opt_args
+typeset -a last_theories
+
+local state line cmd ret=1
+local last_file tmp last_theorie
 
 ##
 _arguments -s -S \
@@ -17,15 +20,15 @@ _arguments -s -S \
      '-'"[Read the input file from stdin]"\
      '*-T'"[<theory> Select <theory> in the input file or in the library]:<theory>:->theories"\
      '*--theory'"[same as -T]:<theory>:->theories"\
-     '*-G'"[<goal> Select <goal> in the last selected theory]:<goal>:"\
-     '*--goal'"[same as -G]:<goal>:"\
+     '*-G'"[<goal> Select <goal> in the last selected theory]:<goal>:->goals"\
+     '*--goal'"[same as -G]:<goal>:->goals"\
      '-C'"[<file> Read configuration from <file>]:Configuration File:_files  -g '*.conf'"\
      '--config'"[same as -C]:Configuration File:_files  -g '*.conf'"\
      "(-L --library -I)"'-L'"[<dir> Add <dir> to the library search path]:Mlpost lib path:_files -/  "\
      "(-L --library -I)"'--library'"[same as -L]:Mlpost lib path:_files -/  "\
      "(-L --library -I)"'-I'"[same as -L (obsolete)]:Mlpost lib path (obsolete use -L):_files -/  "\
      "(-D --driver -P -prover)"'-P'"[<prover> Prove or print (with -o) the selected goals]:<prover>:->provers"\
-     "(-D --driver -P -prover)"'--prover'"[same as -P]:<prover>:compadd $(why3 --list-provers | egrep -E "^  [a-z]"|cut -d' '  -f 3)"\
+     "(-D --driver -P -prover)"'--prover'"[same as -P]:<prover>:->provers"\
      "(-F --format)"'-F'"[<format> Input format (default: \"why\")]:<input format>:"\
      "(-F --format)"'--format'"[same as -F]:<input format>:"\
      "(-t --timelimit)"'-t'"[<sec> Set the prover\'s time limit (default=10, no limit=0)]:<timeout s>:"\
@@ -46,30 +49,61 @@ _arguments -s -S \
      "(--type-only --parse-only -D --driver -P -prover -L --library -I -t --timelimit -m --memlimit)"'--type-only'"[Stop after type checking]"\
      '--debug'"[Set the debug flag]"\
      '*-a'"[<transformation> Add a transformation to apply to the task]:<transformation>:->transforms"\
-     '*--apply-transform'"[same as -a]:<transformation>:compadd $(why3 --list-transforms | grep -e "^  ")"\
+     '*--apply-transform'"[same as -a]:<transformation>:->transforms"\
      "*:The why3 file:->files"\
      && return 0
 
+cmd=$service
 last_file=$line[-1]
+tmp=$opt_args[-T]
+last_theories=(${(s<:>)tmp})
+last_theory=$last_theories[-1]
 
 case $state in
     transforms)
         _message "<transformations>"
-        compadd $(why3 --list-transforms | grep -e "^  ");
+        compadd $($cmd --list-transforms | grep -e "^  ");
         return 0
         ;;
     provers)
         _message "<provers>"
-        compadd $(why3 --list-provers | egrep -E "^  [a-z]"|cut -d' '  -f 3);
+        compadd $($cmd --list-provers | egrep -E "^  [a-z]"|cut -d' '  -f 3);
         return 0
         ;;
     theories)
-        _message "<theories of $last_file>";
-        compadd $(why3 --print-namespace $last_file |grep "^[a-zA-Z]" | cut -d- -f 1);
-        return 1;;
+        tmp=$($cmd --print-namespace $last_file 2> /dev/null);
+        if [[ $? = 0 ]]; then
+            _message "<theories of $last_file>";
+            compadd  $(echo $tmp |grep "^[a-zA-Z]" | cut -d- -f 1);
+            return 0
+        else
+            _message "<invalid file $last_file>";
+            return 1
+        fi;;
+    goals)
+        tmp=$($cmd --print-namespace $last_file -T $last_theory 2> /dev/null);
+        if [[ $? = 0 ]]; then
+            _message "<goals of $last_theory>";
+            compadd  $(echo $tmp |grep -e "-goal" | sed "s/[^-]*-goal //");
+            return 0
+        else
+            _message "<invalid file or theory>";
+            return 1
+        fi;;
     files)
-        _files  -g '*.why';
-        return 1;;
+        case $cmd in
+            why3)
+                _files  -g '*.why';
+                return 0;
+                ;;
+            whyml3)
+                _files  -g '*.{why,mlw}';
+                return 0;
+                ;;
+            *)
+                _message "absurd";
+                return 1;
+        esac;;
     *)
         return 1
 esac

src/core/decl.ml

@@ -487,6 +487,14 @@ let find_prop kn pr =
   | Dprop (_,_,f) -> f
   | _ -> assert false
 
+let find_prop_decl kn pr =
+  match (Mid.find pr.pr_name kn).d_node with
+    | Dind dl ->
+      let test (_,l) = List.mem_assq pr l in
+      Pskip, List.assq pr (snd (List.find test dl))
+  | Dprop (k,_,f) -> k,f
+  | _ -> assert false
+
 exception NonExhaustiveExpr of (pattern list * expr)
 
 let rec check_matchT kn () t = match t.t_node with

src/core/decl.mli

@@ -144,4 +144,5 @@ exception NonExhaustiveExpr of (pattern list * expr)
 val find_constructors : known_map -> tysymbol -> lsymbol list
 val find_inductive_cases : known_map -> lsymbol -> (prsymbol * fmla) list
 val find_prop : known_map -> prsymbol -> fmla
+val find_prop_decl : known_map -> prsymbol -> prop_kind * fmla
 

src/core/pretty.ml

@@ -309,11 +309,13 @@ let print_ind_decl fmt (ps,bl) =
     (print_list newline print_ind) bl;
   forget_tvs ()
 
-let print_pkind fmt = function
-  | Paxiom -> fprintf fmt "axiom"
-  | Plemma -> fprintf fmt "lemma"
-  | Pgoal  -> fprintf fmt "goal"
-  | Pskip  -> fprintf fmt "skip"
+let sprint_pkind = function
+  | Paxiom -> "axiom"
+  | Plemma -> "lemma"
+  | Pgoal  -> "goal"
+  | Pskip  -> "skip"
+
+let print_pkind fmt k = pp_print_string fmt (sprint_pkind k)
 
 let print_prop_decl fmt (k,pr,f) =
   fprintf fmt "@[<hov 2>%a %a : %a@]" print_pkind k
@@ -379,12 +381,14 @@ let print_named_task fmt name task =
 
 module NsTree = struct
   type t =
-    | Namespace of string * namespace
+    | Namespace of string * namespace * known_map
     | Leaf      of string
 
-  let contents ns =
-    let add_ns s ns acc = Namespace (s, ns) :: acc in
-    let add_pr s _  acc = Leaf ("prop " ^ s) :: acc in
+  let contents ns kn =
+    let add_ns s ns acc = Namespace (s, ns, kn) :: acc in
+    let add_pr s p  acc = 
+      let k, _ = find_prop_decl kn p in
+      Leaf (sprint_pkind k ^ " " ^ s) :: acc in
     let add_ls s ls acc =
       if s = "infix ="  && ls_equal ls ps_equ then acc else
       if s = "infix <>" && ls_equal ls ps_neq then acc else
@@ -401,13 +405,14 @@ module NsTree = struct
     let acc = Mnm.fold add_ts ns.ns_ts acc in acc
 
   let decomp = function
-    | Namespace (s,ns) -> s, contents ns
-    | Leaf s           -> s, []
+    | Namespace (s,ns,kn) -> s, contents ns kn
+    | Leaf s              -> s, []
 end
 
-let print_namespace fmt name ns =
+let print_namespace fmt name th =
   let module P = Print_tree.Make(NsTree) in
-  fprintf fmt "@[<hov>%a@]@." P.print (NsTree.Namespace (name, ns))
+  fprintf fmt "@[<hov>%a@]@." P.print 
+    (NsTree.Namespace (name, th.th_export, th.th_known))
 
 (* Exception reporting *)
 

src/core/pretty.mli

@@ -60,5 +60,5 @@ val print_task : formatter -> task -> unit
 val print_theory : formatter -> theory -> unit
 
 val print_named_task : formatter -> string -> task -> unit
-val print_namespace : formatter -> string -> namespace -> unit
+val print_namespace : formatter -> string -> theory -> unit
 

src/main.ml

@@ -268,7 +268,7 @@ let memlimit = match !opt_memlimit with
 let debug = !opt_debug
 
 let print_th_namespace fmt th =
-  Pretty.print_namespace fmt th.th_name.Ident.id_string th.th_export
+  Pretty.print_namespace fmt th.th_name.Ident.id_string th
 
 let fname_printer = ref (Ident.create_ident_printer [])