Basic history support.

builtin_history outputs history, along with a -c option.

Sh_nolog implemented.

Added a simple test, but it's of course non-POSIX because `history` is
an unspecified command. More or less mimicked bash/yash.

src/command.lem

@@ -52,6 +52,7 @@ let builtin_names =
   ; "fg"
   ; "getopts"
   ; "hash"
+  ; "history"
   ; "jobs"
   ; "kill"
   ; "local"
@@ -82,7 +83,7 @@ let is_unspecified_utility s =
           "chdir";"clone";"comparguments";"compcall";"compctl";"compdescribe";
           "compfiles";"compgen";"compgroups";"complete";"compquote";"comptags";
           "comptry";"compvalues";"declare";"dirs";"disable";"disown";"dosh";
-          "echotc";"echoti";(*"help";*)"history";"hist";"let";(*"local";*)"login";
+          "echotc";"echoti";(*"help";*)(*"history";*)"hist";"let";(*"local";*)"login";
           "logout";"map";"mapfile";"popd";"print";"pushd";"readarray";"repeat";
           "savehistory";"source";"shopt";"stop";"suspend";"typeset";"whence"]
 
@@ -2281,11 +2282,65 @@ let builtin_help os0 argv _env =
      Left (os0, "unknown arguments: " ^ string_of_fields argv)
   end
 
-(* TODO 2018-10-01 remaining worthwhile operations *)
-
 (* history *)
+let builtin_history s0 argv _env =
+  (* bash
+history: history [-c] [-d offset] [n] or history -awrn [filename] or history -ps arg [arg...]
+    Display the history list with line numbers.  Lines listed with
+    with a `*' have been modified.  Argument of N says to list only
+    the last N lines.  The `-c' option causes the history list to be
+    cleared by deleting all of the entries.  The `-d' option deletes
+    the history entry at offset OFFSET.  The `-w' option writes out the
+    current history to the history file;  `-r' means to read the file and
+    append the contents to the history list instead.  `-a' means
+    to append history lines from this session to the history file.
+    Argument `-n' means to read all history lines not already read
+    from the history file and append them to the history list.
+    
+    If FILENAME is given, then that is used as the history file else
+    if $HISTFILE has a value, that is used, else ~/.bash_history.
+    If the -s option is supplied, the non-option ARGs are appended to
+    the history list as a single entry.  The -p option means to perform
+    history expansion on each ARG and display the result, without storing
+    anything in the history list.
+    
+    If the $HISTTIMEFORMAT variable is set and not null, its value is used
+    as a format string for strftime(3) to print the time stamp associated
+    with each displayed history entry.  No time stamps are printed otherwise.
+   *)
+  (* yash
+history: manage command history
+
+Syntax:
+	history [-cF] [-d entry] [-s command] [-r file] [-w file] [count]
+
+Options:
+	-c       --clear
+	-d ...   --delete=...
+	-r ...   --read=...
+	-s ...   --set=...
+	-w ...   --write=...
+	-F       --flush-file
+
+Try `man yash' for details.
+   *)
+  match strip_double_dash argv with
+  | [] ->
+     let maxnum = if null s0.sh.history then 0 else maximum (map fst s0.sh.history) in
+     let numwidth = stringLength (stringFromNat maxnum) in
+     let show (num,c) = pad_left (stringFromNat num) numwidth ^ "\t" ^ string_of_stmt c in
+     let msgs = List.reverseMap show s0.sh.history in
+     let s1 = safe_write_stdout "history" (concat "\n" msgs ^ "\n") s0 in
+     Right (exit_with 0 s1, Done)
+  | [[C #'-'; C #'c']] ->
+     Right (exit_with 0 <| s0 with sh = <| s0.sh with history = [] |> |>, Done)
+  | argv' -> Left (s0, "unimplemented option: " ^ string_of_fields argv')
+  end
+
 let builtin_fc = builtin_unimplemented (* needs history, tricky substitution stuff *)
 
+(* TODO 2018-10-01 remaining worthwhile operations *)
+
 (* POSIX user control *)
 let builtin_ulimit = builtin_unimplemented (* XSI *)
 
@@ -2308,6 +2363,7 @@ let builtins =
     ; ("getopts", builtin_getopts)
     ; ("hash", builtin_hash)
     ; ("help", builtin_help)
+    ; ("history", builtin_history)
     ; ("jobs", builtin_jobs)
     ; ("kill", builtin_kill)
 (*    ; ("newgrp", builtin_newgrp) *)

src/os.lem

@@ -337,9 +337,7 @@ let unset_param x os0 =
     export = Set.delete x os1.sh.export
   |> |>
 
-
-
-(* Logging ************************************************************)
+(* Logging and history ************************************************)
 
 val log : forall 'a. log_entry -> os_state 'a -> os_state 'a
 let log entry os = <| os with log = entry::os.log |>
@@ -418,6 +416,43 @@ let log_trace_with write tag msg os0 =
 val log_concretization : forall 'a. symbolic_string -> os_state 'a -> os_state 'a
 let log_concretization ss = log (LogConcretization ss)
 
+val histwrap : forall 'a. os_state 'a -> nat
+let histwrap os =
+  (* When the number reaches an implementation-defined upper limit,
+     which shall be no smaller than the value in HISTSIZE or 32767
+     (whichever is greater), the shell may wrap the numbers, starting
+     the next command with a lower number (usually 1). *)
+  let hard_upper_limit = toNat int32Max in
+  match lookup_concrete_param os "HISTSIZE" with
+  | Nothing -> hard_upper_limit
+  | Just n_str -> 
+     let usr_n =
+       match readUnsignedInteger 10 (toCharList n_str) with
+       | Left _ -> (* yikes? *) hard_upper_limit
+       | Right n -> max (toNat n) 128
+       end
+     in
+     min usr_n hard_upper_limit
+  end
+
+val next_histnum : forall 'a. os_state 'a -> nat
+let next_histnum os =
+  match os.sh.history with
+  | [] -> 1
+  | (last,_)::_ -> 
+     if last = histwrap os
+     then 1
+     else last + 1
+  end
+
+val add_to_history : forall 'a. stmt -> os_state 'a -> os_state 'a
+let add_to_history c os =
+  if Set.member Sh_nolog os.sh.opts
+  then os
+  else
+    let histnum = next_histnum os in
+    <| os with sh = <| os.sh with history = (histnum,c)::os.sh.history |> |>
+
 (* Concretization *****************************************************)
 
 val concretize 

src/semantics.lem

@@ -1354,7 +1354,7 @@ and step_eval s0 checked stmt =
   (* EVALLOOP *****************************************************************)
 
   | EvalLoop linno ((sstr,stackmark) as ctx) src interactive shell_level ->
-     (* INVARIANT: you must call parse_done sstr if you're leaving the eval loop *)
+     (* INVARIANT: you must call parse_cleanup sstr if you're leaving the eval loop *)
      let s1 = show_changed_jobs DeleteJobs Sh_monitor s0 in
      let (s2, parsed) = parse_next s1 interactive stackmark in
      check_traps
@@ -1389,7 +1389,12 @@ and step_eval s0 checked stmt =
            Right (XSEval linno src "empty line", s2, 
                   EvalLoop (linno+1) ctx src interactive shell_level)
         | ParseStmt c ->
-           Right (XSEval linno src "", s2,
+           let s3 = 
+             if is_interactive_mode interactive && is_toplevel shell_level
+             then add_to_history c s2
+             else s2
+           in
+           Right (XSEval linno src "", s3,
                   EvalLoopCmd (linno+1) ctx src interactive shell_level c)
         end)
   | EvalLoopCmd linno ((sstr,_stackmark) as ctx) src interactive shell_level c ->

src/smoosh_prelude.lem

@@ -114,6 +114,9 @@ let pad_right_with c s len =
   let padding = max (len - stringLength s) 0 in
   s ^ toString (replicate padding c) 
 
+val pad_left : string -> nat -> string
+let pad_left = pad_left_with #' '
+
 val pad_right : string -> nat -> string
 let pad_right = pad_right_with #' '
 
@@ -706,10 +709,6 @@ let unimplemented_sh_opts =
   [ (* will not support these *)
     Sh_earlyhash
   ; Sh_vi
-
-    (* TODO 2018-09-10 implement remaining set flags *)
-    (* need history *)
-  ; Sh_nolog
   ]
 
 (**********************************************************************)
@@ -1139,7 +1138,8 @@ and shell_state = <|
     aliases: Map.map string string;
     cwd: string;
     locale: locale;
-    loop_nest: nat (* for tracking break/continue *)
+    loop_nest: nat (* for tracking break/continue *);
+    history: list (nat * stmt)
  |>
 
 val STDIN : fd
@@ -2190,6 +2190,7 @@ let default_shell_state = <|
       aliases = Map.empty;
       cwd = "/";
       locale = lc_ambient;
-      loop_nest = 0
+      loop_nest = 0;
+      history = [];
   |>
 

tests/shell/builtin.history.nonposix.out

@@ -0,0 +1 @@
+ok

tests/shell/builtin.history.nonposix.test

@@ -0,0 +1,15 @@
+cat > scr <<EOF
+history | grep history >/dev/null || exit 1
+echo hi >/dev/null
+history | grep echo >/dev/null || exit 2
+history -c
+history >hist
+grep echo >/dev/null hist && exit 3
+set -o nolog
+history -c
+echo hello >/dev/null
+history >hist2
+grep echo >/dev/null hist2 && exit 4
+echo ok
+EOF
+$TEST_SHELL -i scr 2>/dev/null