To protect your data, the CISO officer has suggested users to enable GitLab 2FA as soon as possible.

Commit c07daecc authored by Michael Norrish's avatar Michael Norrish
Browse files

Merge branch 'master' of gitlab.anu.edu.au:mu/mu-formal-hol

parents fd499b64 ea8b91db
open HolKernel
signature EvalUtils =
sig
val add_extra_eval_thms : unit -> unit
val to_env : term -> term
val start_at : string -> term frag list -> term -> term
val run_schedule : term frag list -> term -> term
val run_finite_schedule : term frag list -> term -> term
val expect_result : term frag list -> term -> thm
val expect_global_value : string -> term frag list -> term -> thm
val take_step : term frag list -> term -> term
val take_steps : term frag list -> term -> term
end
structure EvalUtils :> EvalUtils =
struct
open HolKernel Parse Term boolLib bossLib
open listTheory llistTheory optionTheory pred_setTheory finite_mapTheory uvmMemoryTheory listSyntax stringSyntax
val map_keys_register_fupdate = prove(
``MAP_KEYS (Register (Thread n)) (fm |+ (k, v)) =
MAP_KEYS (Register (Thread n)) fm |+ (Register (Thread n) k, v)``,
simp[INJ_DEF, MAP_KEYS_FUPDATE])
val reduce_o_f_if = prove(
``f x s y y'. (f o_f if x s then y else y') = (if s x then f o_f y else f o_f y')``,
rw[IN_APP])
val in_app_symbolic_only = prove(
``(l: α symbolic). (l P) = P l``,
rw[IN_APP])
val lhdtl_lunfold = prove(
``LHD (LUNFOLD f x) = OPTION_MAP SND (f x)
LTL (LUNFOLD f x) = OPTION_MAP (LUNFOLD f o FST) (f x)``,
rw[] >> rw[Once LUNFOLD, LHDTL_CONS_THM] >>
Cases_on `f x` >> simp[OPTION_MAP_DEF] >> Cases_on `x'` >> simp[])
fun add_extra_eval_thms() : unit =
computeLib.add_funs[
SING, CHOICE_SING,
OPTION_MAP_DEF, OPTION_BIND_def, OPTION_CHOICE_def,
DRESTRICT_FEMPTY, DRESTRICT_FUPDATE,
RRESTRICT_FEMPTY, RRESTRICT_FUPDATE,
FUPDATE_EQ, FUNION_FEMPTY_1, FUNION_FUPDATE_1,
MAP_KEYS_FEMPTY, map_keys_register_fupdate, FCARD_DEF,
o_f_FEMPTY, o_f_FUPDATE, o_f_FUNION, reduce_o_f_if,
in_app_symbolic_only, lhdtl_lunfold]
fun parens q = [QUOTE "("] @ q @ [QUOTE ")"]
fun to_env (bundle : term) : term =
EVAL ``^bundle empty_env`` |> concl |> rhs
fun start_at (func_name : string) (args : term frag list) (env : term) : term =
let val func_name' = fromMLstring func_name in
EVAL(Term(`^env >>= λe. init_sched_state <|env:=e;main:=Func ^func_name';args:=` @ parens args @ `|>`))
|> concl |> rhs
end
fun run_schedule (schedule : term frag list) (state : term) : term =
EVAL(Term(`^state >>= run_schedule` @ parens schedule)) |> concl |> rhs
fun run_finite_schedule (schedule : term frag list) (state : term) : term =
EVAL(Term(`^state >>= run_finite_schedule` @ parens schedule)) |> concl |> rhs
fun expect_result (expected : term frag list) (state : term) : thm =
let val actual = EVAL(``^state >>= get_return_values``) |> concl |> rhs
in prove(Term(parens expected @ ` = ^actual`), simp[]) end
fun expect_global_value (name : string) (value : term frag list) (state : term) : thm =
let val actual = EVAL(``^state >>= get_global_value ^(fromMLstring name)``) |> concl |> rhs
in prove(Term(parens value @ ` = ^actual`), simp[]) end
fun take_step (step : term frag list) (state : term) : term =
EVAL(Term(`^state >>= take_step` @ parens step)) |> concl |> rhs
fun take_steps (steps : term frag list) (state : term) : term =
EVAL(Term(`^state >>= take_steps` @ parens steps)) |> concl |> rhs
end
INCLUDES = $(CMLDIR) $(CMLDIR)/translator/ $(CMLDIR)/candle/standard/ml_kernel/ $(CMLDIR)/explorer/pp/astPP $(HOLDIR)/examples/formal-languages/context-free/ $(CMLDIR)/compiler/parsing
# Evaluation function testing on toy language
# Evaluation function testing on toy expression language
## Alexander Soen
exprEvalScript.sml
- defines the grammer of the expression language and the standard evaluation function for it
exprScheduleScript.sml
- defines a scheduler function which finds valids schedules for a defined program
- defines an evaluation function which evaluates a program by n steps
exprTestScript.sml
- a set of test programs and schedules for the standard evaluation function
ml\_hol\_exprProgScript.sml
- translation of all functions from the above scripts
ppExprScript.sml
- pretty prints the translated functions into a sml format in a text file
### References
Expression language - $(HOLDIR)/examples/opsemTools/newOpsemScript.sml
Translation and pretty printing - $(CMLDIR)/candle/standard/ml\_kernel
......@@ -4,18 +4,10 @@
Alexander Soen
*)
open HolKernel bossLib Parse boolLib
open HolKernel bossLib Parse boolLib;
open listTheory alistTheory stringTheory;
open stringTheory
open alistTheory
(* abbrevations *)
(*
val _ = type_abbrev ("env", ``:(string # expr) list``)
val _ = type_abbrev ("posn", ``:bool list``)
*)
val _ = new_theory "extExpr"
val _ = new_theory "exprEval";
(* Language definition *)
val _ = Datatype`
......@@ -42,6 +34,7 @@ val _ = Datatype`
| Eq expr expr
`
(* Fixity of operators *)
val _ = set_mapped_fixity { term_name = "Seq", fixity = Infixl 500, tok = ";;"}
val _ = set_mapped_fixity { term_name = "Parallel", fixity = Infixl 500, tok = "||"}
val _ = set_mapped_fixity { term_name = "Plus", fixity = Infixl 500, tok = "+_"}
......@@ -57,6 +50,10 @@ val _ = Datatype`
| R
`
(* Do Ning value *)
val N_def = Define`
N = L
`
(* List helper functions *)
(* Update *)
val update_env_def = Define`
......@@ -66,6 +63,7 @@ val update_env_def = Define`
| T => (s1, c1) :: rst
| F => (s2, c2) :: (update_env (s1, c1) rst))
`
(* Remove *)
val remove_env_def = Define`
(remove_env str [] = NONE)
......@@ -75,78 +73,83 @@ val remove_env_def = Define`
| SOME env' => SOME ((s, c) :: env')))
`
(* Translate ALOOKUP for use *)
(* Step Evaluation *)
(* start expression level *)
val eval_xpr_step_def = Define`
(eval_xpr_step (Var str) env [] =
val eval_expr_step_def = Define`
(eval_expr_step (Var str) env [] =
case ALOOKUP env str of
| NONE => NONE
| SOME res => SOME (Const res))
(eval_xpr_step (Plus (Const num1) (Const num2)) env [] =
(eval_expr_step (Plus (Const num1) (Const num2)) env [] =
SOME (Const (num1 + num2)))
(eval_xpr_step (Plus xpr1 xpr2) env posn =
(eval_expr_step (Plus xpr1 xpr2) env posn =
case posn of
| (L::rest) => (case eval_xpr_step xpr1 env rest of
| (L::rest) => (case eval_expr_step xpr1 env rest of
| NONE => NONE
| SOME xpr1' => SOME (Plus xpr1' xpr2))
| (R::rest) => (case eval_xpr_step xpr2 env rest of
| (R::rest) => (case eval_expr_step xpr2 env rest of
| NONE => NONE
| SOME xpr2' => SOME (Plus xpr1 xpr2'))
| _ => NONE)
(eval_xpr_step (Times (Const num1) (Const num2)) env [] =
(eval_expr_step (Times (Const num1) (Const num2)) env [] =
SOME (Const (num1 * num2)))
(eval_xpr_step (Times xpr1 xpr2) env posn =
(eval_expr_step (Times xpr1 xpr2) env posn =
case posn of
| (L::rest) => (case eval_xpr_step xpr1 env rest of
| (L::rest) => (case eval_expr_step xpr1 env rest of
| NONE => NONE
| SOME xpr1' => SOME (Times xpr1' xpr2))
| (R::rest) => (case eval_xpr_step xpr2 env rest of
| (R::rest) => (case eval_expr_step xpr2 env rest of
| NONE => NONE
| SOME xpr2' => SOME (Times xpr1 xpr2'))
| _ => NONE)
(eval_xpr_step _ _ _ = NONE)
(eval_expr_step _ _ _ = NONE)
`
(* end expression level *)
(* start boolean level *)
val eval_bool_step_def = Define`
(eval_bool_step (Lt (Const num1) (Const num2)) env [] =
val eval_bexpr_step_def = Define`
(eval_bexpr_step (Lt (Const num1) (Const num2)) env [] =
if num1 < num2 then SOME True else SOME False)
(eval_bool_step (Lt xpr1 xpr2) env posn =
(eval_bexpr_step (Lt xpr1 xpr2) env posn =
case posn of
| (L::rest) => (case eval_xpr_step xpr1 env rest of
| (L::rest) => (case eval_expr_step xpr1 env rest of
| NONE => NONE
| SOME xpr1' => SOME (Lt xpr1' xpr2))
| (R::rest) => (case eval_xpr_step xpr2 env rest of
| (R::rest) => (case eval_expr_step xpr2 env rest of
| NONE => NONE
| SOME xpr2' => SOME (Lt xpr1 xpr2'))
| _ => NONE)
(eval_bool_step (Gt (Const num1) (Const num2)) env [] =
(eval_bexpr_step (Gt (Const num1) (Const num2)) env [] =
if num1 > num2 then SOME True else SOME False)
(eval_bool_step (Gt xpr1 xpr2) env posn =
(eval_bexpr_step (Gt xpr1 xpr2) env posn =
case posn of
| (L::rest) => (case eval_xpr_step xpr1 env rest of
| (L::rest) => (case eval_expr_step xpr1 env rest of
| NONE => NONE
| SOME xpr1' => SOME (Gt xpr1' xpr2))
| (R::rest) => (case eval_xpr_step xpr2 env rest of
| (R::rest) => (case eval_expr_step xpr2 env rest of
| NONE => NONE
| SOME xpr2' => SOME (Gt xpr1 xpr2'))
| _ => NONE)
(eval_bool_step (Eq (Const num1) (Const num2)) env [] =
(eval_bexpr_step (Eq (Const num1) (Const num2)) env [] =
if num1 = num2 then SOME True else SOME False)
(eval_bool_step (Eq xpr1 xpr2) env posn =
(eval_bexpr_step (Eq xpr1 xpr2) env posn =
case posn of
| (L::rest) => (case eval_xpr_step xpr1 env rest of
| (L::rest) => (case eval_expr_step xpr1 env rest of
| NONE => NONE
| SOME xpr1' => SOME (Eq xpr1' xpr2))
| (R::rest) => (case eval_xpr_step xpr2 env rest of
| (R::rest) => (case eval_expr_step xpr2 env rest of
| NONE => NONE
| SOME xpr2' => SOME (Eq xpr1 xpr2'))
| _ => NONE)
(eval_bool_step _ _ _ = NONE)
(eval_bexpr_step _ _ _ = NONE)
`
(* end boolean level *)
(* start program level *)
val eval_step_def = Define`
(eval_step (Assign str xpr) env posn =
......@@ -154,7 +157,7 @@ val eval_step_def = Define`
| [] => (case xpr of
| Const c => SOME (Skip, update_env (str, c) env)
| _ => NONE)
| (_::rest) => (case eval_xpr_step xpr env rest of
| (_::rest) => (case eval_expr_step xpr env rest of
| NONE => NONE
| SOME xpr' => SOME (Assign str xpr', env)))
(eval_step (Free str) env [] =
......@@ -176,7 +179,7 @@ val eval_step_def = Define`
| True => SOME (stmt1, env)
| False => SOME (stmt2, env)
| _ => NONE)
| (_::rest) => (case eval_bool_step g env rest of
| (_::rest) => (case eval_bexpr_step g env rest of
| NONE => NONE
| SOME xpr => SOME (Elf xpr stmt1 stmt2, env)))
(eval_step (While g b) env posn =
......@@ -197,8 +200,8 @@ val eval_step_def = Define`
(* Schedule evaluation *)
val eval_scheduler_def = Define`
eval_scheduler stmt env scheduler =
case scheduler of
eval_scheduler stmt env schedule =
case schedule of
| [] => SOME (stmt, env)
| (sch::rest) => (case eval_step stmt env sch of
| NONE => NONE
......
(*
Scheduler script which finds valid schedules in a program
Alexander Soen
*)
open HolKernel bossLib Parse boolLib;
open pairTheory listTheory stringTheory alistTheory;
open exprEvalTheory;
val _ = new_theory "exprSchedule";
(* finds the steps for expr stmts *)
val find_expr_steps_def = Define`
(find_expr_steps (Var str) env step = if (ALOOKUP env str = NONE) then NONE else SOME [step])
(find_expr_steps ((Const _) +_ (Const _)) _ step = SOME [step])
(find_expr_steps ((Const _) ×_ (Const _)) _ step = SOME [step])
(find_expr_steps (lexpr +_ rexpr) env step =
case (find_expr_steps lexpr env (step ++ [L]), find_expr_steps rexpr env (step ++ [R])) of
| (NONE , NONE ) => NONE
| (SOME res1, NONE ) => SOME res1
| (NONE , SOME res2) => SOME res2
| (SOME res1, SOME res2) => SOME (res1 ++ res2))
(find_expr_steps (lexpr ×_ rexpr) env step =
case (find_expr_steps lexpr env (step ++ [L]), find_expr_steps rexpr env (step ++ [R])) of
| (NONE , NONE ) => NONE
| (SOME res1, NONE ) => SOME res1
| (NONE , SOME res2) => SOME res2
| (SOME res1, SOME res2) => SOME (res1 ++ res2))
(find_expr_steps _ _ _ = NONE)
`
(* finds the steps for bexpr stmts *)
val find_bexpr_steps_def = Define`
(find_bexpr_steps ((Const _) <_ (Const _)) _ step = SOME [step])
(find_bexpr_steps ((Const _) >_ (Const _)) _ step = SOME [step])
(find_bexpr_steps ((Const _) =_ (Const _)) _ step = SOME [step])
(find_bexpr_steps (lexpr <_ rexpr) env step =
case (find_expr_steps lexpr env (step ++ [L]), find_expr_steps rexpr env (step ++ [R])) of
| (NONE , NONE ) => NONE
| (SOME res1, NONE ) => SOME res1
| (NONE , SOME res2) => SOME res2
| (SOME res1, SOME res2) => SOME (res1 ++ res2))
(find_bexpr_steps (lexpr >_ rexpr) env step =
case (find_expr_steps lexpr env (step ++ [L]), find_expr_steps rexpr env (step ++ [R])) of
| (NONE , NONE ) => NONE
| (SOME res1, NONE ) => SOME res1
| (NONE , SOME res2) => SOME res2
| (SOME res1, SOME res2) => SOME (res1 ++ res2))
(find_bexpr_steps (lexpr =_ rexpr) env step =
case (find_expr_steps lexpr env (step ++ [L]), find_expr_steps rexpr env (step ++ [R])) of
| (NONE , NONE ) => NONE
| (SOME res1, NONE ) => SOME res1
| (NONE , SOME res2) => SOME res2
| (SOME res1, SOME res2) => SOME (res1 ++ res2))
(find_bexpr_steps _ _ _ = NONE)
`
(* finds the steps for general stmts *)
val find_steps_def = Define`
(find_steps (Assign _ (Const _)) _ step = SOME [step])
(find_steps (Free str) env step = if (remove_env str env = NONE) then NONE else SOME [step])
(find_steps (Skip || Skip) _ step = SOME [step])
(find_steps (Elf True _ _) _ step = SOME [step])
(find_steps (Elf False _ _) _ step = SOME [step])
(find_steps (While _ _) _ step = SOME [step])
(find_steps (Skip ;; _) _ step = SOME [step])
(find_steps (Assign _ expr) env step = find_expr_steps expr env (step ++ [N]))
(find_steps (stmt ;; _) env step = find_steps stmt env (step ++ [N]))
(find_steps (Elf bexpr _ _) env step = find_bexpr_steps bexpr env (step ++ [N]))
(find_steps (lstmt || rstmt) env step =
case (find_steps lstmt env (step ++ [L]), find_steps rstmt env (step ++ [R])) of
| (NONE , NONE ) => NONE
| (SOME res1, NONE ) => SOME res1
| (NONE , SOME res2) => SOME res2
| (SOME res1, SOME res2) => SOME (res1 ++ res2))
(find_steps _ _ _ = NONE)
`
(* evaluates the a program by n steps using the scheduler function *)
val eval_n_steps_def = Define`
(eval_n_steps prog env 0 = SOME (prog, env))
(eval_n_steps prog env (SUC n) =
case find_steps prog env [] of
| NONE => NONE
| SOME (schedule::_) => case eval_step prog env schedule of
| NONE => NONE
| SOME res => eval_n_steps (FST res) (SND res) n)
`
(*
Not evaluating the OPTION_BIND function
val eval_n_steps_def = Define`
(eval_n_steps prog env 0 = SOME (prog, env)) ∧
(eval_n_steps Skip env _ = NONE) ∧
(eval_n_steps prog env (SUC n) =
case find_steps prog env [] of
| NONE => NONE
| SOME schedule => (OPTION_BIND (eval_step prog env (HD schedule)) (λopt . eval_n_steps (FST opt) (SND opt) n)))
`
*)
(*
Example test case: EVAL ``eval_n_steps fac_prog [("n", 2)] 41``;
TODO:
prove ∀ p e. (find_steps p e [] = SOME steps) ⇒ ∃ s. eval_step p e s = SOME res
Trying to prove that the find_steps functions will not produce SOME []
g` ∀ prog env step_acc. (find_expr_steps prog env step_acc = SOME steps) ⇒ steps ≠ []`
e (Induct_on `prog`)
e (EVAL_TAC)
e (Cases_on `ALOOKUP env s`)
e (rw [])
e (rw [])
e (EVAL_TAC)
e (rw [])
e (`find_expr_steps (prog +_ prog') env [] = (
case (find_expr_steps prog env ([L]), find_expr_steps prog' env ([R])) of
| (NONE , NONE ) => NONE
| (SOME res1, NONE ) => SOME res1
| (NONE , SOME res2) => SOME res2
| (SOME res1, SOME res2) => SOME (res1 ++ res2))` by rw [find_expr_steps_def])
e (Cases_on `find_expr_steps prog env ([L])`)
e (Cases_on `find_expr_steps prog' env ([R])`)
e (EVAL_TAC)
(**)
e (Cases_on `find_expr_steps prog env step_acc`)
e (Cases_on `find_expr_steps prog' env step_acc`)
e (metis_tac [find_expr_steps_def])
g` ∀ prog env. (find_steps prog env [] = SOME steps) ⇒ steps ≠ []`
g` ∀ p e. (find_steps p e [] = SOME steps) ⇒ eval_step p e (HD steps) = SOME res`
g` ∀ p e. (find_steps p e [] = SOME steps) ⇒ ∃ s. eval_step p e s = SOME res`
*)
val _ = export_theory ()
(*
Parse script to turn S-expressions into the defined language's datatype
Alexander Soen
*)
open HolKernel bossLib Parse boolLib;
open stringTheory;
open exprEvalTheory;
open simpleSexpTheory fromSexpTheory;
open monadsyntax;
val _ = new_theory "exprSexp";
val _ = temp_add_monadsyntax ();
val _ = temp_overload_on ("return", ``SOME``);
(* Stripping functions to remove the S-sexpression syntax *)
val strstrip_sexp_def = Define`
(strstrip_sexp (SX_STR str) = SOME str)
(strstrip_sexp _ = NONE)
`
val numstrip_sexp_def = Define`
(numstrip_sexp (SX_NUM num) = SOME num)
(numstrip_sexp _ = NONE)
`
(* Termination proof required due to recursion *)
val sexp2expr_def = tDefine "sexp2expr" `
sexp2expr s =
case dstrip_sexp s of
| SOME ("Var", [str]) =>
do
sl <- strstrip_sexp str;
return (Var sl)
od
| SOME ("Const", [num]) =>
do
nl <- numstrip_sexp num;
return (Const nl)
od
| SOME ("Plus", [expr1;expr2]) => (
case (sexp2expr expr1, sexp2expr expr2) of
| (SOME e1, SOME e2) => SOME (Plus e1 e2)
| _ => NONE)
| SOME ("Times", [expr1;expr2]) => (
case (sexp2expr expr1, sexp2expr expr2) of
| (SOME e1, SOME e2) => SOME (Times e1 e2)
| _ => NONE)
| _ => NONE
` (WF_REL_TAC `measure sexp_size` >> rw [] >> simp [dstrip_sexp_size])
(* Uses the measure on the size of the s-expression and then uses an
already proven property that dstrip_sexp will always decrease the
size of an sexpression *)
val sexp2bexpr_def = Define`
sexp2bexpr s =
case dstrip_sexp s of
| SOME ("True", []) => SOME True
| SOME ("False", []) => SOME False
| SOME ("Lt", [expr1; expr2]) => (
case (sexp2expr expr1, sexp2expr expr2) of
| (SOME e1, SOME e2) => SOME (Lt e1 e2)
| _ => NONE)
| SOME ("Gt", [expr1; expr2]) => (
case (sexp2expr expr1, sexp2expr expr2) of
| (SOME e1, SOME e2) => SOME (Gt e1 e2)
| _ => NONE)
| SOME ("Eq", [expr1; expr2]) => (
case (sexp2expr expr1, sexp2expr expr2) of
| (SOME e1, SOME e2) => SOME (Eq e1 e2)
| _ => NONE)
| _ => NONE
`
val sexp2stmt_def = tDefine "sexp2stmt" `
sexp2stmt s =
case dstrip_sexp s of
| SOME ("Skip", []) => SOME Skip
| SOME ("Assign", [str; expr]) =>
do
sl <- strstrip_sexp str;
e <- sexp2expr expr;
return (Assign sl e)
od
| SOME ("Free", [str]) =>
do
sl <- strstrip_sexp str;
return (Free sl)
od
| SOME ("Parallel", [stmt1; stmt2]) => (
case (sexp2stmt stmt1, sexp2stmt stmt2) of
| (SOME s1, SOME s2) => SOME (Parallel s1 s2)
| _ => NONE)
| SOME ("Elf", [bexpr; stmt1; stmt2]) => (
case (sexp2bexpr bexpr, sexp2stmt stmt1, sexp2stmt stmt2) of
| (SOME b, SOME s1, SOME s2) => SOME (Elf b s1 s2)
| _ => NONE)
| SOME ("Seq", [stmt1; stmt2]) => (
case (sexp2stmt stmt1, sexp2stmt stmt2) of
| (SOME s1, SOME s2) => SOME (Seq s1 s2)
| _ => NONE)
| SOME ("While", [bexpr; stmt]) => (
case (sexp2bexpr bexpr, sexp2stmt stmt) of
| (SOME b, SOME s) => SOME (While b s)
| _ => NONE)
| _ => NONE
` (WF_REL_TAC `measure sexp_size` >> rw [] >> simp [dstrip_sexp_size])
(* --- *)
(* Alternative definitions using "do" notation,
Does not translate
val sexp2expr_do_def = tDefine "sexp2expr_do" `
sexp2expr_do s =
case dstrip_sexp s of
| SOME ("Var", [str]) =>
do
sl <- strstrip_sexp str;
return (Var sl)
od
| SOME ("Const", [num]) =>
do
nl <- numstrip_sexp num;
return (Const nl)
od
| SOME ("Plus", [expr1;expr2]) =>
do