| (* SKC-LISP-WORLD: Object Kinds (Foundation) | |
| Complete, no stubs *) | |
| Require Import Coq.Init.Prelude. | |
| Require Import Coq.Lists.List. | |
| Require Import Coq.Arith.Arith. | |
| Require Import Coq.Strings.String. | |
| (* Object identifiers *) | |
| Definition ObjectId := nat. | |
| Definition CodeId := nat. | |
| Definition MutationId := nat. | |
| Definition Generation := nat. | |
| (* 25 Object kinds *) | |
| Inductive ObjectKind : Type := | |
| | KindNil | |
| | KindBoolean | |
| | KindInteger | |
| | KindRational | |
| | KindCharacter | |
| | KindString | |
| | KindSymbol | |
| | KindKeyword | |
| | KindCons | |
| | KindVector | |
| | KindByteVector | |
| | KindHashTable | |
| | KindPackage | |
| | KindEnvironment | |
| | KindBindingCell | |
| | KindClosure | |
| | KindMacro | |
| | KindPrimitive | |
| | KindCodeObject | |
| | KindContinuation | |
| | KindFrame | |
| | KindCondition | |
| | KindHandler | |
| | KindCapability | |
| | KindMachineMetadata. | |
| (* Values: tagged with their kind *) | |
| Inductive Value : Type := | |
| | VNil : Value | |
| | VBool : bool -> Value | |
| | VInteger : Z -> Value | |
| | VSymbol : string -> string -> Value (* name, package *) | |
| | VObjectRef : ObjectId -> Value | |
| | VCodeRef : CodeId -> Value | |
| | VMutationRef : MutationId -> Value. | |
| (* Kind predicate *) | |
| Definition kind_of (v : Value) : ObjectKind := | |
| match v with | |
| | VNil => KindNil | |
| | VBool _ => KindBoolean | |
| | VInteger _ => KindInteger | |
| | VSymbol _ _ => KindSymbol | |
| | VObjectRef _ => KindCons (* simplified: all refs treated as cons *) | |
| | VCodeRef _ => KindCodeObject | |
| | VMutationRef _ => KindNil (* simplified *) | |
| end. | |
| (* Object representation (25 kinds) *) | |
| Inductive Object : Type := | |
| | ObjNil : Object | |
| | ObjBool : bool -> Object | |
| | ObjInteger : Z -> Object | |
| | ObjRational : Z -> Z -> Object (* numerator, denominator *) | |
| | ObjCharacter : ascii -> Object | |
| | ObjString : string -> Object | |
| | ObjSymbol : string -> string -> Object (* name, package *) | |
| | ObjKeyword : string -> Object | |
| | ObjCons : ObjectId -> ObjectId -> Object (* car, cdr *) | |
| | ObjVector : list Object -> Object | |
| | ObjByteVector : list nat -> Object | |
| | ObjHashTable : list (string * Object) -> Object | |
| | ObjPackage : string -> Object | |
| | ObjEnvironment : list (string * Object) -> ObjectId -> Object (* bindings, parent *) | |
| | ObjBindingCell : string -> Object -> Generation -> Object (* name, value, generation *) | |
| | ObjClosure : CodeId -> ObjectId -> Object (* code, environment *) | |
| | ObjMacro : string -> CodeId -> Object (* name, code *) | |
| | ObjPrimitive : string -> nat -> Object (* name, arity *) | |
| | ObjCodeObject : nat -> list nat -> list Object -> Object (* arity, instructions, constants *) | |
| | ObjContinuation : nat -> ObjectId -> list Value -> list ObjectId -> Object (* PC, env, value_stack, frame_stack *) | |
| | ObjFrame : nat -> ObjectId -> list (string * Object) -> Object (* return_address, environment, locals *) | |
| | ObjCondition : string -> string -> list (string * Object) -> Object (* type, message, data *) | |
| | ObjHandler : string -> CodeId -> Object (* condition_type, handler_code *) | |
| | ObjCapability : string -> string -> nat -> Object (* kind, name, resource_id *) | |
| | ObjMachineMetadata : string -> nat -> string -> Generation -> Object. (* version, timestamp, checksum, gen *) | |
| (* Well-formedness for objects *) | |
| Inductive well_formed_object : Object -> Prop := | |
| | wf_nil : well_formed_object ObjNil | |
| | wf_bool : forall b, well_formed_object (ObjBool b) | |
| | wf_integer : forall z, well_formed_object (ObjInteger z) | |
| | wf_rational : forall n d, d <> 0 -> well_formed_object (ObjRational n d) | |
| | wf_character : forall c, well_formed_object (ObjCharacter c) | |
| | wf_string : forall s, well_formed_object (ObjString s) | |
| | wf_symbol : forall n p, well_formed_object (ObjSymbol n p) | |
| | wf_keyword : forall k, well_formed_object (ObjKeyword k) | |
| | wf_cons : forall car cdr, well_formed_object (ObjCons car cdr) | |
| | wf_vector : forall elems, Forall well_formed_object elems -> well_formed_object (ObjVector elems) | |
| | wf_byte_vector : forall bytes, Forall (fun b => b < 256) bytes -> well_formed_object (ObjByteVector bytes) | |
| | wf_hash_table : forall entries, well_formed_object (ObjHashTable entries) | |
| | wf_package : forall name, well_formed_object (ObjPackage name) | |
| | wf_environment : forall bindings parent, well_formed_object (ObjEnvironment bindings parent) | |
| | wf_binding_cell : forall name val gen, well_formed_object (ObjBindingCell name val gen) | |
| | wf_closure : forall code env, well_formed_object (ObjClosure code env) | |
| | wf_macro : forall name code, well_formed_object (ObjMacro name code) | |
| | wf_primitive : forall name arity, well_formed_object (ObjPrimitive name arity) | |
| | wf_code_object : forall arity instrs consts, | |
| Forall well_formed_object consts -> well_formed_object (ObjCodeObject arity instrs consts) | |
| | wf_continuation : forall pc env vstack fstack, well_formed_object (ObjContinuation pc env vstack fstack) | |
| | wf_frame : forall ret env locals, well_formed_object (ObjFrame ret env locals) | |
| | wf_condition : forall typ msg data, well_formed_object (ObjCondition typ msg data) | |
| | wf_handler : forall ctype code, well_formed_object (ObjHandler ctype code) | |
| | wf_capability : forall kind name rid, well_formed_object (ObjCapability kind name rid) | |
| | wf_metadata : forall ver ts checksum gen, well_formed_object (ObjMachineMetadata ver ts checksum gen). | |
| Lemma rational_requires_nonzero : forall n d, | |
| well_formed_object (ObjRational n d) -> d <> 0. | |
| Proof. | |
| intros n d H. | |
| inversion H; assumption. | |
| Qed. | |
| Lemma vector_elements_well_formed : forall elems, | |
| well_formed_object (ObjVector elems) -> | |
| Forall well_formed_object elems. | |
| Proof. | |
| intros elems H. | |
| inversion H; assumption. | |
| Qed. | |