Permalink
Browse files

Merge pull request #597 from CakeML/lem-194778e

Lem 194778e
  • Loading branch information...
xrchz committed Jan 9, 2019
2 parents f298b17 + 482b551 commit b19ca63f5f4b645ed5c3cc20d17301531d25408d
@@ -4,9 +4,6 @@ with Lem requires)
[lem_list_extraScript.sml](lem_list_extraScript.sml):
This is a file that is required for Lem to work.

[lem_map_extraScript.sml](lem_map_extraScript.sml):
This is a file that is required for Lem to work.

[lem_pervasivesScript.sml](lem_pervasivesScript.sml):
This is a file that is required for Lem to work.

@@ -16,9 +13,6 @@ This is a file that is required for Lem to work.
[lem_set_extraScript.sml](lem_set_extraScript.sml):
This is a file that is required for Lem to work.

[lem_show_extraScript.sml](lem_show_extraScript.sml):
This is a file that is required for Lem to work.

[lem_stringScript.sml](lem_stringScript.sml):
This is a file that is required for Lem to work.

This file was deleted.

Oops, something went wrong.

This file was deleted.

Oops, something went wrong.
@@ -1,9 +1,8 @@
(*
Extensions to Lem's built-in library to target things we need in HOL.
*)

open import Pervasives
import List_extra
import String

(* TODO: look for these in the built-in library *)

@@ -1,6 +1,6 @@
(*Generated by Lem from lib.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_pervasivesTheory lem_list_extraTheory lem_stringTheory alistTheory llistTheory locationTheory sptreeTheory wordsTheory integer_wordTheory;
open lem_pervasivesTheory alistTheory llistTheory locationTheory sptreeTheory wordsTheory integer_wordTheory;

val _ = numLib.prefer_num();

@@ -11,9 +11,8 @@ val _ = new_theory "lib"
(*
Extensions to Lem's built-in library to target things we need in HOL.
*)

(*open import Pervasives*)
(*import List_extra*)
(*import String*)

(* TODO: look for these in the built-in library *)

@@ -25,20 +24,20 @@ val _ = new_theory "lib"
(*val map2 : forall 'a 'b 'c. ('a -> 'b -> 'c) -> list 'a -> list 'b -> list 'c*)

val _ = Define `
(the _ (SOME x)= x) /\ (the x NONE= x)`;
((the:'a -> 'a option -> 'a) _ (SOME x)= x) /\ ((the:'a -> 'a option -> 'a) x NONE= x)`;


(*val fapply : forall 'a 'b. MapKeyType 'b => 'a -> 'b -> Map.map 'b 'a -> 'a*)
val _ = Define `
(fapply d x f= ((case FLOOKUP f x of SOME d => d | NONE => d )))`;
((fapply:'a -> 'b ->('b,'a)fmap -> 'a) d x f= ((case FLOOKUP f x of SOME d => d | NONE => d )))`;


val lunion_defn = Defn.Hol_multi_defns `

(lunion [] s= s)
((lunion:'a list -> 'a list -> 'a list) [] s= s)
/\
(lunion (x::xs) s=
(if MEM x s
((lunion:'a list -> 'a list -> 'a list) (x::xs) s=
(if MEM x s
then lunion xs s
else x::(lunion xs s)))`;

@@ -116,8 +115,8 @@ val _ = type_abbrev((* ( 'a, 'b) *) "alist" , ``: ('a # 'b) list``);

(*val opt_bind : forall 'a 'b. maybe 'a -> 'b -> alist 'a 'b -> alist 'a 'b*)
val _ = Define `
(opt_bind n v e=
((case n of
((opt_bind:'a option -> 'b ->('a#'b)list ->('a#'b)list) n v e=
((case n of
NONE => e
| SOME n' => (n',v)::e
)))`;
@@ -127,8 +126,8 @@ val _ = Define `

val _ = Define `

(lshift (n : num) ls=
(MAP (\ v . v - n) (FILTER (\ v . n <= v) ls)))`;
((lshift:num ->(num)list ->(num)list) (n : num) ls=
(MAP (\ v . v - n) (FILTER (\ v . n <= v) ls)))`;


(*open import {hol} `locationTheory`*)
@@ -1,6 +1,8 @@
(*
Definition of CakeML abstract syntax (AST).
*)

open import Pervasives_extra
open import Pervasives
open import Lib
open import Namespace
@@ -1,6 +1,6 @@
(*Generated by Lem from ast.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_pervasivesTheory libTheory namespaceTheory fpSemTheory;
open lem_pervasivesTheory lem_pervasives_extraTheory libTheory namespaceTheory fpSemTheory;

val _ = numLib.prefer_num();

@@ -13,6 +13,8 @@ val _ = set_grammar_ancestry ["integer", "words", "string", "namespace", "locati
(*
Definition of CakeML abstract syntax (AST).
*)

(*open import Pervasives_extra*)
(*open import Pervasives*)
(*open import Lib*)
(*open import Namespace*)
@@ -1,6 +1,6 @@
(*Generated by Lem from evaluate.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_pervasives_extraTheory libTheory astTheory namespaceTheory ffiTheory semanticPrimitivesTheory;
open lem_pervasives_extraTheory libTheory namespaceTheory astTheory semanticPrimitivesTheory ffiTheory;

val _ = numLib.prefer_num();

@@ -231,8 +231,8 @@ val _ = Lib.with_flag (computeLib.auto_import_definitions, false) (List.map Defn
))
)))
/\
(evaluate_decs st env [Dlocal lds ds]=
((case evaluate_decs st env lds of
((evaluate_decs:'ffi state ->(v)sem_env ->(dec)list -> 'ffi state#(((v)sem_env),(v))result) st env [Dlocal lds ds]=
((case evaluate_decs st env lds of
(st1, Rval env1) =>
evaluate_decs st1 (extend_dec_env env1 env) ds
| res => res
@@ -16,8 +16,6 @@ val _ = new_theory "ffi"
(*open import Pervasives_extra*)
(*open import Lib*)

(* An oracle says how to perform an ffi call based on its internal state,
* represented by the type variable 'ffi. *)

val _ = Hol_datatype `
ffi_outcome = FFI_failed | FFI_diverged`;
@@ -51,7 +49,7 @@ val _ = Hol_datatype `

(*val initial_ffi_state : forall 'ffi. oracle 'ffi -> 'ffi -> ffi_state 'ffi*)
val _ = Define `
(initial_ffi_state oc ffi=
((initial_ffi_state:(string -> 'ffi oracle_function) -> 'ffi -> 'ffi ffi_state) oc ffi=
(<| oracle := oc
; ffi_state := ffi
; io_events := ([])
@@ -64,15 +62,15 @@ val _ = Hol_datatype `

(*val call_FFI : forall 'ffi. ffi_state 'ffi -> string -> list word8 -> list word8 -> ffi_result 'ffi*)
val _ = Define `
(call_FFI st s conf bytes=
(if ~ (s = "") then
((call_FFI:'ffi ffi_state -> string ->(word8)list ->(word8)list -> 'ffi ffi_result) st s conf bytes=
(if ~ (s = "") then
(case st.oracle s st.ffi_state conf bytes of
Oracle_return ffi' bytes' =>
if LENGTH bytes' = LENGTH bytes then
(FFI_return
( st with<| ffi_state := ffi'
; io_events :=
(st.io_events ++
(st.io_events ++
[IO_event s conf (ZIP (bytes, bytes'))])
|>)
bytes')
@@ -110,8 +108,8 @@ val _ = Hol_datatype `

(*val trace_oracle : oracle (llist io_event)*)
val _ = Define `
(trace_oracle s io_trace conf input=
((case LHD io_trace of
((trace_oracle:string ->(io_event)llist ->(word8)list ->(word8)list ->((io_event)llist)oracle_result) s io_trace conf input=
((case LHD io_trace of
SOME (IO_event s' conf' bytes2) =>
if (s = s') /\ (MAP FST bytes2 = input) /\ (conf = conf') then
Oracle_return (THE (LTL io_trace)) (MAP SND bytes2)
@@ -120,3 +118,4 @@ val _ = Define `
)))`;

val _ = export_theory()

@@ -22,17 +22,17 @@ val _ = Hol_datatype `

(*val isEof : oracle_function simpleIO*)
val _ = Define `
(isEof st conf input=
((case input of
((isEof:simpleIO ->(word8)list ->(word8)list ->(simpleIO)oracle_result) st conf input=
((case input of
[] => Oracle_final FFI_failed
| x::xs => Oracle_return st ((if st.input = LNIL then n2w (( 1 : num)) else n2w (( 0 : num)))::xs)
)))`;


(*val getChar : oracle_function simpleIO*)
val _ = Define `
(getChar st conf input=
((case input of
((getChar:simpleIO ->(word8)list ->(word8)list ->(simpleIO)oracle_result) st conf input=
((case input of
[] => Oracle_final FFI_failed
| x::xs =>
(case LHD st.input of
@@ -44,22 +44,22 @@ val _ = Define `

(*val putChar : oracle_function simpleIO*)
val _ = Define `
(putChar st conf input=
((case input of
((putChar:simpleIO ->(word8)list ->(word8)list ->(simpleIO)oracle_result) st conf input=
((case input of
[] => Oracle_final FFI_failed
| x::_ => Oracle_return (( st with<| output := (LCONS x st.output) |>)) input
)))`;


(*val exit : oracle_function simpleIO*)
val _ = Define `
(exit st conf input= (Oracle_final FFI_diverged))`;
((exit:simpleIO ->(word8)list ->(word8)list ->(simpleIO)oracle_result) st conf input= (Oracle_final FFI_diverged))`;


(*val simpleIO_oracle : oracle simpleIO*)
val _ = Define `
(simpleIO_oracle s st conf input=
(if s = "isEof" then
((simpleIO_oracle:string -> simpleIO ->(word8)list ->(word8)list ->(simpleIO)oracle_result) s st conf input=
(if s = "isEof" then
isEof st conf input
else if s = "getChar" then
getChar st conf input
@@ -71,3 +71,4 @@ val _ = Define `
Oracle_final FFI_failed))`;

val _ = export_theory()

@@ -1,6 +1,6 @@
(*Generated by Lem from primTypes.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_pervasivesTheory libTheory astTheory namespaceTheory ffiTheory semanticPrimitivesTheory evaluateTheory typeSystemTheory;
open lem_pervasivesTheory libTheory namespaceTheory astTheory semanticPrimitivesTheory ffiTheory evaluateTheory typeSystemTheory;

val _ = numLib.prefer_num();

@@ -1,6 +1,6 @@
(*Generated by Lem from semanticPrimitives.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_pervasivesTheory lem_list_extraTheory lem_stringTheory libTheory lem_string_extraTheory astTheory namespaceTheory ffiTheory fpSemTheory;
open lem_pervasivesTheory libTheory namespaceTheory fpSemTheory astTheory ffiTheory lem_list_extraTheory lem_stringTheory lem_string_extraTheory;

val _ = numLib.prefer_num();

@@ -1,6 +1,6 @@
(*Generated by Lem from typeSystem.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_pervasives_extraTheory libTheory astTheory namespaceTheory semanticPrimitivesTheory;
open lem_pervasives_extraTheory libTheory namespaceTheory astTheory semanticPrimitivesTheory;

val _ = numLib.prefer_num();

0 comments on commit b19ca63

Please sign in to comment.