# HOL-Theorem-Prover/HOL

### Subversion checkout URL

You can clone with
or
.

# Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also compare across forks.

# Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also compare across forks.
...
• 3 commits
• 4 files changed
• 1 contributor
Commits on Feb 28, 2012
 Scott Owens `Fix the miniML type soundness proof for =` `eefe62f` Scott Owens `Started a printer for the miniML AST` `ddbb571` Scott Owens `Merge branch 'master' of github.com:mn200/HOL` `1bb14db`
2  examples/miniML/MiniMLScript.sml
 @@ -1103,7 +1103,7 @@ val _ = Define ` (Opapp, Tfn t2' t3', _) => (t2 = t2') /\ (t3 = t3') | (Opn _, Tnum, Tnum) => (t3 = Tnum) | (Opb _, Tnum, Tnum) => (t3 = Tbool) - | (Equality, t1, t2) => (t1 = t2) + | (Equality, t1, t2) => (t1 = t2) /\ (t3 = Tbool) | _ => F ))`;
2  examples/miniML/miniML.lem
 @@ -1005,7 +1005,7 @@ let type_op op t1 t2 t3 = | (Opapp, Tfn t2' t3', _) -> (t2 = t2') && (t3 = t3') | (Opn _, Tnum, Tnum) -> (t3 = Tnum) | (Opb _, Tnum, Tnum) -> (t3 = Tbool) - | (Equality, t1, t2) -> (t1 = t2) + | (Equality, t1, t2) -> (t1 = t2) && (t3 = Tbool) | _ -> false end
134 examples/miniML/print_ast.lem
 @@ -0,0 +1,134 @@ +open MiniML + +val num_to_string : num -> string + +let infixes = [] + +let rec +list_to_string printer sep [] = + "" +and +list_to_string printer sep [x] = + printer x +and +list_to_string printer sep (x::y::l) = + printer x ^ sep ^ printer y ^ list_to_string printer sep l + +let lit_to_string l = match l with + (* Rely on the fact that true and false cannot be rebound in SML *) + | Bool true -> "true" + | Bool false -> "false" + | Num n -> num_to_string n +end + +let var_to_string v = + if List.assoc v infixes then + "op " ^ v + else + v + +let rec +pat_to_string (Pvar v) = var_to_string v +and +pat_to_string (Plit l) = lit_to_string l +and +pat_to_string (Pcon None ps) = "(" ^ list_to_string pat_to_string "," ps ^ ")" +and +pat_to_string (Pcon (Some c) []) = + var_to_string c +and +pat_to_string (Pcon (Some c) ps) = + "(" ^ var_to_string c ^ "(" ^ list_to_string pat_to_string "," ps ^ ")" ^ ")" + +let rec +exp_to_string (Raise r) = + "(raise Bind)" +and +exp_to_string (Val (Lit l)) = + lit_to_string l +and +exp_to_string (Val _) = + (* TODO: this shouldn't happen in source *) + "" +and +exp_to_string (Con None es) = "(" ^ list_to_string exp_to_string "," es ^ ")" +and +exp_to_string (Con (Some c) []) = + var_to_string c +and +exp_to_string (Con (Some c) es) = + "(" ^ var_to_string c ^ "(" ^ list_to_string exp_to_string "," es ^ ")" ^ ")" +and +exp_to_string (Var v) = + var_to_string v +and +exp_to_string (Fun v e) = + "(fn " ^ var_to_string v ^ " => " ^ exp_to_string e ^ ")" +and +exp_to_string (App Opapp e1 e2) = + "(" ^ exp_to_string e1 ^ " " ^ exp_to_string e2 ^ ")" +and +exp_to_string (App Equality e1 e2) = + (* Rely on the fact (?) that = cannot be rebound in SML *) + "(" ^ exp_to_string e1 ^ " = " ^ exp_to_string e2 ^ ")" +and +exp_to_string (App (Opn o) e1 e2) = + "" + (* TODO: Make the op not a function + if List.assoc o infixes then + "(" ^ exp_to_string e1 ^ " " ^ o ^ " " ^ exp_to_string e2 ^ ")" + else + "(" ^ o " " ^ exp_to_string e1 ^ " " exp_to_string e2 ^ ")" + *) +and +exp_to_string (App (Opb o) e1 e2) = + "" + (* TODO: Make the op not a function + if List.assoc o infixes then + "(" ^ exp_to_string e1 ^ " " ^ o ^ " " ^ exp_to_string e2 ^ ")" + else + "(" ^ o " " ^ exp_to_string e1 ^ " " exp_to_string e2 ^ ")" + *) +and +exp_to_string (Log l e1 e2) = + "(" ^ exp_to_string e1 ^ (if l = And then " andalso " else " orelse ") ^ + exp_to_string e2 ^ ")" +and +exp_to_string (If e1 e2 e3) = + "(if " ^ exp_to_string e1 ^ " then " ^ exp_to_string e2 ^ " else " ^ + exp_to_string e3 ^ ")" +and +exp_to_string (Mat e pes) = + "(case " ^ exp_to_string e ^ " of " ^ + list_to_string pat_exp_to_string "|" pes ^ ")" +and +exp_to_string (Let v e1 e2) = + "(let val " ^ var_to_string v ^ " = " ^ exp_to_string e1 ^ " in " ^ + exp_to_string e2 ^ " end)" +and +exp_to_string (Letrec funs e) = + "(let fun " ^ list_to_string fun_to_string " and " funs ^ " in " ^ + exp_to_string e ^ " end)" +and +pat_exp_to_string (p,e) = + pat_to_string p ^ " => " ^ exp_to_string e +and +fun_to_string (v1,v2,e) = + var_to_string v1 ^ " " ^ var_to_string v2 ^ " = " ^ exp_to_string e + +let variant_to_string (c,ts) = + var_to_string c ^ (if ts = [] then "" else " of " (* TODO *)) + +let type_to_string (tvs, name, variants) = + (if tvs = [] then "" else "(" ^ list_to_string (fun x -> x) "," tvs ^ ")") ^ + name ^ " = " ^ list_to_string variant_to_string "|" variants + +let rec +dec_to_string (Dlet p e) = + "val " ^ pat_to_string p ^ " = " ^ exp_to_string e +and +dec_to_string (Dletrec funs) = + "fun " ^ list_to_string fun_to_string " and " funs +and +dec_to_string (Dtype types) = + "datatype " ^ list_to_string type_to_string " and " types
11 examples/miniML/typeSoundScript.sml
 @@ -365,7 +365,8 @@ val type_op_cases = Q.prove ( type_op op t1 t2 t3 = ((∃op'. op = Opn op') ∧ (t1 = Tnum) ∧ (t2 = Tnum) ∧ (t3 = Tnum)) ∨ ((∃op'. op = Opb op') ∧ (t1 = Tnum) ∧ (t2 = Tnum) ∧ (t3 = Tbool)) ∨ - ((op = Opapp) ∧ (t1 = Tfn t2 t3))`, + ((op = Opapp) ∧ (t1 = Tfn t2 t3)) ∨ + ((op = Equality) ∧ (t1 = t2) ∧ (t3 = Tbool))`, rw [type_op_def] >> every_case_tac >> fs [] >> @@ -733,6 +734,14 @@ rw [] >| metis_tac [], every_case_tac >> fs [] >> + rw [type_e_val] >> + fs [hd (CONJUNCTS type_v_cases)] >> + rw [] >> + fs [type_op_cases] >> + rw [] >> + metis_tac [], + every_case_tac >> + fs [] >> rw [type_e_val] >| [qpat_assum `type_v tenvC (Closure l s e) t1'` (ASSUME_TAC o SIMP_RULE (srw_ss()) [Once type_v_cases]) >>

### No commit comments for this range

Something went wrong with that request. Please try again.