Changeset 2645 for src/joint


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
Location:
src/joint
Files:
4 edited
1 moved

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2595 r2645  
    77include "common/LabelledObjects.ma".
    88include "ASM/Util.ma".
     9include "joint/String.ma".
    910
    1011(* Here is the structure of parameter records (downward edges are coercions,
     
    108109  | extension_seq : ext_seq p → joint_seq p globals.
    109110
    110 axiom EmptyString : String.
    111111definition NOOP ≝ λp,globals.COMMENT p globals EmptyString.
    112112
  • src/joint/String.ma

    r2643 r2645  
    1 include "basics/lists/list.ma".
     1include "basics/pts.ma".
    22
    3 include "ASM/Char.ma".
    4 
    5 definition String ≝ list Char.
     3(* Stupid definition, just to avoid an axiom in the extracted code *)
     4(* Strings at the moment are only used in comments in the back-end *)
     5axiom String: Type[0] ≝
     6   EmptyString : String.
  • src/joint/Traces.ma

    r2642 r2645  
    6666coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params
    6767≝ make_global on _p : prog_params to evaluation_params.
    68 
    69 axiom BadMain : String.
    7068
    7169definition make_initial_state :
  • 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.
  • src/joint/semanticsUtils.ma

    r2601 r2645  
    4646; stackp : xpointer
    4747}.
    48 
    49 axiom BadRegister : String.
    5048
    5149definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
Note: See TracChangeset for help on using the changeset viewer.