Ignore:
Timestamp:
Feb 7, 2013, 9:22:22 PM (7 years ago)
Author:
sacerdot
Message:
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/joint_semantics.ma

    r2641 r2645  
    3939| both_is : beval → beval → internal_stack.
    4040
    41 axiom InternalStackFull : String.
    42 axiom InternalStackEmpty : String.
    43 
    4441definition is_push : internal_stack → beval → res internal_stack ≝
    4542λis,bv.match is with
     
    108105 λp,frms,st. mk_state … frms (istack … st) (carry … st) (regs … st) (m … st).
    109106
    110 axiom BadProgramCounter : String.
    111 
    112107(*
    113108inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
     
    122117  | FEnd2  : fin_step_flow p F Call. (* end flow *)
    123118*)
    124 
    125 axiom ProgramCounterOutOfCode : String.
    126 axiom PointNotFound : String.
    127 axiom LabelNotFound : String.
    128 axiom MissingSymbol : String.
    129 axiom FailedLoad : String.
    130 axiom BadFunction : String.
    131 axiom SuccessorNotProvided : String.
    132 axiom BadPointer : String.
    133119
    134120(* this can replace graph_fetch function and lin_fetch_function *)
     
    256242    return set_regs ? r st.
    257243 
    258 axiom FailedStore: String.
    259 
    260244definition push: ∀p.state p → beval → res (state p) ≝
    261245 λp,st,v.
     
    402386 set_pc … newpc st.
    403387
    404 axiom NoSuccessor : String.
    405388definition next_of_call_pc : ∀p : sem_params.∀globals.genv_t (joint_function p globals) →
    406389  program_counter → res (succ p) ≝
     
    524507      set_result … p vs dest st.
    525508
    526 axiom MissingStackSize : String.
    527 
    528509definition eval_internal_call ≝
    529510λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
     
    691672% qed.
    692673
    693 axiom ExternalMain: String.
    694 
    695674definition make_initial_state :
    696675 ∀pars: sem_params.
Note: See TracChangeset for help on using the changeset viewer.