Changeset 2645 for src/LIN


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/LIN
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN.ma

    r2537 r2645  
    3636    (* ext_seq_labels ≝ *) ltl_lin_seq_labels
    3737    (* has_tailcalls ≝ *) false
    38     (* paramsT ≝ *) unit
    39     (* localsT ≝ *) void.
     38    (* paramsT ≝ *) unit.
    4039
    4140interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).
  • src/LIN/joint_LTL_LIN_semantics.ma

    r2443 r2645  
    11include "LIN/joint_LTL_LIN.ma".
    2 include "joint/SemanticUtils.ma".
     2include "joint/semanticsUtils.ma".
    33
    44definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e).
     
    77  λl,a.match a with
    88  [ Reg r ⇒ hw_reg_retrieve l r
    9   | Imm b ⇒ OK … b
     9  | Imm b ⇒ OK … (BVByte b)
    1010  ].
    1111
     
    1717  hw_reg_store RegisterA (hwreg_retrieve e r) e
    1818| int_to_reg r v ⇒
    19   hw_reg_store r v e
     19  hw_reg_store r (BVByte v) e
    2020| int_to_acc _ v ⇒
    21   hw_reg_store RegisterA v e
     21  hw_reg_store RegisterA (BVByte v) e
    2222].
    2323
     
    5555  (* snd_arg_retrieve_  ≝ *) hw_arg_retrieve
    5656  (* pair_reg_move_     ≝ *) eval_registers_move
    57   (* fetch_ra           ≝ *) (load_ra …)
     57(*  (* fetch_ra           ≝ *) (load_ra …)
    5858  (* allocate_local     ≝ *) (λabs.match abs in void with [ ])
    59   (* save_frame         ≝ *) (λp.λ_.λst.save_ra … st p)
     59*)  (* save_frame         ≝ *) ?(*(λp.λ_.λst.save_ra … st p)*)
    6060  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
    61   (* fetch_external_args≝ *) ltl_lin_fetch_external_args
     61  (* fetch_external_args≝ *) ?(*ltl_lin_fetch_external_args*)
    6262  (* set_result         ≝ *) ltl_lin_set_result
    6363  (* call_args_for_main ≝ *) 0
     
    6565  (* read_result        ≝ *) (λ_.λ_.λ_.
    6666  λst.return map … (hwreg_retrieve (regs … st)) RegisterRets)
    67   (* eval_ext_seq       ≝ *) (λ_.λ_.λs.λ_.eval_ltl_lin_seq s)
    68   (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
     67  (* eval_ext_seq       ≝ *) ?(*(λ_.λ_.λs.λ_.eval_ltl_lin_seq s)*)
     68(*  (* eval_ext_tailcall  ≝ *) ?(*(λ_.λ_.λabs.match abs in void with [ ])*)
    6969  (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
    70   (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st)
    71   (* post_op2           ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st).
     70*)  (* pop_frame          ≝ *) ?(*(λ_.λ_.λ_.λst.return st)*)
     71(*  (* post_op2           ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)*).
Note: See TracChangeset for help on using the changeset viewer.