text:
Require Import Kami.StateMonad Kami.Syntax Kami.Properties Kami.PProperties Kami.PPlusProperties Kami.Notations Kami.Lib.EclecticLib.
Import Word.Notations.

Require Import ZArith.

Set Implicit Arguments.
Set Asymmetric Patterns.

Section Compile.
  Variable ty: Kind -> Type.
  Variable regMapTy: Type.

  Inductive RegMapExpr: Type :=
  | VarRegMap (v: regMapTy): RegMapExpr
  | UpdRegMap (r: string) (pred: Bool @# ty) (k: FullKind) (val: Expr ty k)
              (regMap: RegMapExpr): RegMapExpr
  | CompactRegMap (regMap: RegMapExpr): RegMapExpr.

  Inductive CompActionT: Kind -> Type :=
  | CompCall (f: string) (argRetK: Kind * Kind) (pred: Bool @# ty)
             (arg: fst argRetK @# ty)
             lret (cont: fullType ty (SyntaxKind (snd argRetK)) -> CompActionT lret): CompActionT lret
  | CompLetExpr k (e: Expr ty k) lret (cont: fullType ty k -> CompActionT lret): CompActionT lret
  | CompNondet k lret (cont: fullType ty k -> CompActionT lret): CompActionT lret
  | CompSys (pred: Bool @# ty) (ls: list (SysT ty)) lret (cont: CompActionT lret): CompActionT lret
  | CompRead (r: string) (k: FullKind) (readMap: RegMapExpr) lret (cont: fullType ty k -> CompActionT lret): CompActionT lret
  | CompRet lret (e: lret @# ty) (newMap: RegMapExpr) : CompActionT lret
  | CompLetFull k (a: CompActionT k) lret (cont: fullType ty (SyntaxKind k) -> regMapTy -> CompActionT lret): CompActionT lret
  | CompAsyncRead (idxNum num : nat) (readPort dataArray writePort: string) (isWriteMask: bool)
                  (idx : Bit (Nat.log2_up idxNum) @# ty) (pred : Bool @# ty) (k : Kind) (writeMap readMap : RegMapExpr) lret
                  (cont : fullType ty (SyntaxKind (Array num k)) -> regMapTy -> CompActionT lret) : CompActionT lret
  | CompWrite (idxNum num : nat) (writePort dataArray : string) (idx  : Bit (Nat.log2_up idxNum) @# ty) (Data : Kind) (val : Array num Data @# ty)
              (mask : option (Array num Bool @# ty)) (pred : Bool @# ty) (writeMap readMap : RegMapExpr) lret
              (cont : regMapTy -> CompActionT lret) : CompActionT lret
  | CompSyncReadReq (idxNum num : nat) (readReq readReg dataArray : string) (idx : Bit (Nat.log2_up idxNum) @# ty) (Data : Kind)
                    (isAddr : bool) (pred : Bool @# ty) (writeMap readMap : RegMapExpr) lret
                    (cont : regMapTy -> CompActionT lret) : CompActionT lret
  | CompSyncReadRes (idxNum num : nat) (readResp readReg dataArray writePort : string) (isWriteMask: bool)
                    (Data : Kind) (isAddr : bool) (writeMap readMap : RegMapExpr) lret
                    (cont : fullType ty (SyntaxKind (Array num Data)) -> regMapTy -> CompActionT lret) : CompActionT lret.

  Inductive EActionT (lretT : Kind) : Type :=
  | EMCall (meth : string) s (e : Expr ty (SyntaxKind (fst s)))
           (cont : (fullType ty (SyntaxKind (snd s))) -> EActionT lretT) : EActionT lretT
  | ELetExpr (k : FullKind) (e : Expr ty k) (cont : fullType ty k  -> EActionT lretT) : EActionT lretT
  | ELetAction (k : Kind) (a : EActionT k) (cont : fullType ty (SyntaxKind k) -> EActionT lretT) : EActionT lretT
  | EReadNondet (k : FullKind) (cont : fullType ty k -> EActionT lretT) : EActionT lretT
  | EReadReg (r : string) (k : FullKind) (cont : fullType ty k -> EActionT lretT) : EActionT lretT
  | EWriteReg (r : string) (k : FullKind) (e :  Expr ty k) (cont : EActionT lretT) : EActionT lretT
  | EIfElse : Expr ty (SyntaxKind Bool) -> forall k, EActionT k -> EActionT k -> (fullType ty (SyntaxKind k) -> EActionT lretT) -> EActionT lretT
  | ESys (ls : list (SysT ty)) (cont : EActionT lretT) : EActionT lretT
  | EReturn (e : Expr ty (SyntaxKind lretT)) : EActionT lretT
  | EAsyncRead (idxNum num : nat) (readPort dataArray writePort : string) (isWriteMask: bool) (idx : Bit (Nat.log2_up idxNum) @# ty)
                      (k : Kind) (cont : fullType ty (SyntaxKind (Array num k)) -> EActionT lretT) : EActionT lretT
  | EWrite (idxNum num : nat) (write dataArray : string) (idx : Bit (Nat.log2_up idxNum) @# ty)
                  (Data : Kind) (val : Array num Data @# ty) (mask : option (Array num Bool @# ty))
                  (cont : EActionT lretT) : EActionT lretT
  | ESyncReadReq (idxNum num : nat) (readReq readReg dataArray : string) (idx : Bit (Nat.log2_up idxNum) @# ty)
                        (Data : Kind) (isAddr : bool) (cont : EActionT lretT) : EActionT lretT
  | ESyncReadRes (idxNum num : nat) (readRes readReg dataArray writePort: string) (isWriteMask: bool) (Data : Kind) (isAddr : bool)
                        (cont : fullType ty (SyntaxKind (Array num Data)) -> EActionT lretT) : EActionT lretT.

  Fixpoint Action_EAction (lretT : Kind) (a : ActionT ty lretT) :  EActionT lretT :=
    match a in ActionT _ _ with
    | MCall meth k argExpr cont =>
      EMCall meth k argExpr (fun v => Action_EAction (cont v))
    | Return x =>
      EReturn x
    | LetExpr k' expr cont => ELetExpr expr (fun v => Action_EAction (cont v))
    | ReadNondet k' cont => EReadNondet k' (fun ret => Action_EAction (cont ret))
    | Sys ls cont => ESys ls (Action_EAction cont)
    | ReadReg r k' cont => EReadReg r k' (fun v => Action_EAction (cont v))
    | WriteReg r k' expr cont => EWriteReg r expr (Action_EAction cont)
    | LetAction k' a' cont => ELetAction (Action_EAction a') (fun v => Action_EAction (cont v))
    | IfElse pred' k' aT aF cont => EIfElse pred' (Action_EAction aT) (Action_EAction aF) (fun v => Action_EAction (cont v))
    end.

  Section ReadMap.
    Variable readMap: regMapTy.

    Fixpoint compileAction k (a: ActionT ty k) (pred: Bool @# ty)
             (writeMap: RegMapExpr) {struct a}:
      CompActionT k :=
      match a in ActionT _ _ with
      | MCall meth k argExpr cont =>
        CompCall meth k pred argExpr (fun ret => @compileAction _ (cont ret) pred writeMap)
      | Return x =>
        CompRet x writeMap
      | LetExpr k' expr cont => CompLetExpr expr (fun ret => @compileAction _ (cont ret) pred writeMap)
      | ReadNondet k' cont => CompNondet k' (fun ret => @compileAction _ (cont ret) pred writeMap)
      | Sys ls cont => CompSys pred ls (compileAction cont pred writeMap)
      | ReadReg r k' cont =>
        @CompRead r k' (VarRegMap readMap) _ (fun v => @compileAction _ (cont v) pred writeMap)
      | WriteReg r k' expr cont =>
        CompLetFull (CompRet ($$ WO)%kami_expr
                             (UpdRegMap r pred expr writeMap)) (fun _ v => @compileAction _ cont pred (VarRegMap v))
      | LetAction k' a' cont =>
        CompLetFull (@compileAction k' a' pred writeMap)
                    (fun retval writeMap' => @compileAction k (cont retval) pred (VarRegMap writeMap'))
      | IfElse pred' k' aT aF cont =>
        CompLetExpr
          (pred && pred')%kami_expr
          (fun truePred =>
             CompLetExpr
               (pred && !pred')%kami_expr
               (fun falsePred =>
                  CompLetFull (@compileAction k' aT (#truePred)%kami_expr writeMap)
                              (fun valT writesT =>
                                 CompLetFull (@compileAction k' aF (#falsePred)%kami_expr (VarRegMap writesT))
                                             (fun valF writesF =>
                                                CompLetExpr (IF pred' then #valT else #valF)%kami_expr
                                                            (fun val => (@compileAction k (cont val) pred (VarRegMap writesF)))
                              ))))
      end.

    Fixpoint EcompileAction k (a : EActionT k) (pred : Bool @# ty)
             (writeMap : RegMapExpr) {struct a} :
      CompActionT k :=
      match a in EActionT _ with
      | EMCall meth k argExpr cont =>
        CompCall meth k pred argExpr (fun ret => @EcompileAction _ (cont ret) pred writeMap)
      | EReturn x =>
        CompRet x writeMap
      | ELetExpr k' expr cont => CompLetExpr expr (fun ret => @EcompileAction _ (cont ret) pred writeMap)
      | EReadNondet k' cont => CompNondet k' (fun ret => @EcompileAction _ (cont ret) pred writeMap)
      | ESys ls cont => CompSys pred ls (EcompileAction cont pred writeMap)
      | EReadReg r k' cont =>
        @CompRead r k' (VarRegMap readMap) _ (fun v => @EcompileAction _ (cont v) pred writeMap)
      | EWriteReg r k' expr cont =>
        CompLetFull (CompRet ($$ WO)%kami_expr
                             (UpdRegMap r pred expr writeMap)) (fun _ v => @EcompileAction _ cont pred (VarRegMap v))
      | ELetAction k' a' cont =>
        CompLetFull (@EcompileAction k' a' pred writeMap)
                    (fun retval writeMap' => @EcompileAction k (cont retval) pred (VarRegMap writeMap'))
      | EIfElse pred' k' aT aF cont =>
        CompLetExpr
          (pred && pred')%kami_expr
          (fun truePred =>
             CompLetExpr
               (pred && !pred')%kami_expr
               (fun falsePred =>
                  CompLetFull (@EcompileAction k' aT (#truePred)%kami_expr writeMap)
                              (fun valT writesT =>
                                 CompLetFull (@EcompileAction k' aF (#falsePred)%kami_expr (VarRegMap writesT))
                                             (fun valF writesF =>
                                                CompLetExpr (IF pred' then #valT else #valF)%kami_expr
                                                            (fun val => (@EcompileAction k (cont val) pred (VarRegMap writesF)))
                              ))))
      | EAsyncRead idxNum num readPort dataArray writePort isWriteMask idx k cont =>
        CompAsyncRead idxNum readPort dataArray writePort isWriteMask idx pred writeMap (VarRegMap readMap)
                      (fun array writeMap' => @EcompileAction _ (cont array) pred (VarRegMap writeMap'))
      | EWrite idxNum num writePort dataArray idx Data val mask cont =>
        CompWrite idxNum writePort  dataArray idx val mask pred writeMap (VarRegMap readMap)
                  (fun writeMap' => @EcompileAction _ cont pred (VarRegMap writeMap'))
      | ESyncReadReq idxNum num readReq readReg dataArray idx Data isAddr cont =>
        CompSyncReadReq idxNum num readReq readReg dataArray idx Data isAddr pred writeMap (VarRegMap readMap)
                        (fun writeMap' => @EcompileAction _ cont pred (VarRegMap writeMap'))
      | ESyncReadRes idxNum num readResp readReg dataArray writePort isWriteMask Data isAddr cont =>
        CompSyncReadRes idxNum readResp readReg dataArray writePort isWriteMask isAddr writeMap (VarRegMap readMap)
                        (fun array writeMap' => @EcompileAction _ (cont array) pred (VarRegMap writeMap'))
      end.

    Fixpoint inlineWriteFile k (rf : RegFileBase) (a : EActionT k) : EActionT k :=
      match rf with
      | @Build_RegFileBase _isWrMask _num _dataArray _readers _write _idxNum _Data _init =>
        match a with
        | EMCall g sign arg cont =>
          match String.eqb _write g with
          | true =>
            if _isWrMask then
              match Signature_dec sign (WriteRqMask (Nat.log2_up _idxNum) _num _Data, Void) with
              | left isEq =>
                let inValue := (match isEq in _ = Y return Expr ty (SyntaxKind (fst Y)) with | eq_refl => arg end) in
                ELetExpr ($$ WO)%kami_expr
                         (fun v => EWrite _idxNum _write _dataArray (inValue @% "addr")%kami_expr (inValue @% "data")%kami_expr
                                          (Some (inValue @% "mask")%kami_expr) (inlineWriteFile rf (match isEq in _ = Y return fullType ty (SyntaxKind (snd Y)) -> EActionT k with
                                                                                | eq_refl => cont
                                                                                end v)))
              | right _ => EMCall g sign arg (fun ret => inlineWriteFile rf (cont ret))
              end
            else
              match Signature_dec sign (WriteRq (Nat.log2_up _idxNum) (Array _num _Data), Void) with
              | left isEq =>
                let inValue := (match isEq in _ = Y return Expr ty (SyntaxKind (fst Y)) with | eq_refl => arg end) in
                ELetExpr ($$ WO)%kami_expr
                         (fun v => EWrite _idxNum _write _dataArray (inValue @% "addr")%kami_expr (inValue @% "data")%kami_expr
                                          None (inlineWriteFile rf (match isEq in _ = Y return fullType ty (SyntaxKind (snd Y)) -> EActionT k with
                                                                    | eq_refl => cont
                                                                    end v)))
              | right _ => EMCall g sign arg (fun ret => inlineWriteFile rf (cont ret))
              end
          | false => EMCall g sign arg (fun ret => inlineWriteFile rf (cont ret))
          end
        | ELetExpr _ e cont => ELetExpr e (fun ret => inlineWriteFile rf (cont ret))
        | ELetAction _ a cont => ELetAction (inlineWriteFile rf a) (fun ret => inlineWriteFile rf (cont ret))
        | EReadNondet k c => EReadNondet k (fun ret => inlineWriteFile rf (c ret))
        | EReadReg r k c => EReadReg r k (fun ret => inlineWriteFile rf (c ret))
        | EWriteReg r k e a => EWriteReg r e (inlineWriteFile rf a)
        | EIfElse p _ aT aF c => EIfElse p (inlineWriteFile rf aT) (inlineWriteFile rf aF) (fun ret => inlineWriteFile rf (c ret))
        | ESys ls c => ESys ls (inlineWriteFile rf c)
        | EReturn e => EReturn e
        | EAsyncRead idxNum num readPort dataArray writePort isWriteMask idx k cont =>
          EAsyncRead idxNum readPort dataArray writePort isWriteMask idx (fun ret => inlineWriteFile rf (cont ret))
        | EWrite idxNum num writePort dataArray idx Data val mask cont =>
          EWrite idxNum writePort dataArray idx val mask (inlineWriteFile rf cont)
        | ESyncReadReq idxNum num readReq readReg dataArray idx Data isAddr cont =>
          ESyncReadReq idxNum num readReq readReg dataArray idx Data isAddr (inlineWriteFile rf cont)
        | ESyncReadRes idxNum num readResp readReg dataArray writePort isWriteMask Data isAddr cont =>
          ESyncReadRes idxNum readResp readReg dataArray writePort isWriteMask isAddr (fun v => inlineWriteFile rf (cont v))
        end
      end.

    Fixpoint inlineAsyncReadFile (read : string) (rf : RegFileBase) k (a : EActionT k) : EActionT k :=
      match rf with
      | @Build_RegFileBase _isWrMask _num _dataArray _readers _write _idxNum _Data _init =>
        match _readers with
        | Async reads =>
          match (existsb (String.eqb read) reads) with
          | true =>
            match a with
            | EMCall g sign arg cont =>
              match String.eqb read g with
              | true =>
                match Signature_dec sign (Bit (Nat.log2_up _idxNum), Array _num _Data) with
                | left isEq =>
                  let inValue := (match isEq in _ = Y return Expr ty (SyntaxKind (fst Y)) with | eq_refl => arg end) in
                  EAsyncRead _idxNum read _dataArray _write _isWrMask inValue
                             (fun array =>
                                inlineAsyncReadFile  read rf (match isEq in _ = Y return
                                                                    fullType ty (SyntaxKind (snd Y)) -> EActionT k with
                                                              | eq_refl => cont
                                                              end array))
                | right _ => EMCall g sign arg (fun ret => inlineAsyncReadFile read rf (cont ret))
                end
              | false => EMCall g sign arg (fun ret => inlineAsyncReadFile read rf (cont ret))
              end
            | ELetExpr _ e cont => ELetExpr e (fun ret => inlineAsyncReadFile read rf (cont ret))
            | ELetAction _ a cont => ELetAction (inlineAsyncReadFile read rf a) (fun ret => inlineAsyncReadFile read rf (cont ret))
            | EReadNondet k c => EReadNondet k (fun ret => inlineAsyncReadFile read rf (c ret))
            | EReadReg r k c => EReadReg r k (fun ret => inlineAsyncReadFile read rf (c ret))
            | EWriteReg r k e a => EWriteReg r e (inlineAsyncReadFile read rf a)
            | EIfElse p _ aT aF c => EIfElse p (inlineAsyncReadFile read rf aT) (inlineAsyncReadFile read rf aF) (fun ret => inlineAsyncReadFile read rf (c ret))
            | ESys ls c => ESys ls (inlineAsyncReadFile read rf c)
            | EReturn e => EReturn e
            | EAsyncRead idxNum num readPort dataArray writePort isWriteMask idx k cont =>
              EAsyncRead idxNum readPort dataArray writePort isWriteMask idx (fun ret => inlineAsyncReadFile read rf (cont ret))
            | EWrite idxNum num writePort dataArray idx Data val mask cont =>
              EWrite idxNum writePort dataArray idx val mask (inlineAsyncReadFile read rf cont)
            | ESyncReadReq idxNum num readReq readReg dataArray idx Data isAddr cont =>
              ESyncReadReq idxNum num readReq readReg dataArray idx Data isAddr (inlineAsyncReadFile read rf cont)
            | ESyncReadRes idxNum num readResp readReg dataArray writePort isWriteMask Data isAddr cont =>
              ESyncReadRes idxNum readResp readReg dataArray writePort isWriteMask isAddr (fun v => inlineAsyncReadFile read rf (cont v))
            end
          | false => a
          end
        | Sync _ _ => a
        end
      end.

  Lemma SyncRead_eq_dec (r r' : SyncRead) :
    {r = r'} + {r <> r'}.
  Proof.
    destruct (string_dec (readReqName r) (readReqName r')),
    (string_dec (readResName r) (readResName r')),
    (string_dec (readRegName r) (readRegName r')), r, r';
      simpl in *; subst; auto; right; intro; inv H; auto.
  Qed.

  Definition SyncRead_eqb (r r' : SyncRead) : bool :=
    (String.eqb (readReqName r) (readReqName r'))
      && (String.eqb (readResName r) (readResName r'))
      && (String.eqb (readRegName r) (readRegName r')).

  Lemma SyncRead_eqb_eq (r r' : SyncRead) :
    SyncRead_eqb r r' = true <-> r = r'.
  Proof.
    split; intros.
    - unfold SyncRead_eqb in H.
      repeat (apply andb_prop in H; dest; rewrite String.eqb_eq in *).
      destruct r, r'; simpl in *; subst; auto.
    - rewrite H.
      unfold SyncRead_eqb; repeat rewrite eqb_refl; auto.
  Qed.

  Fixpoint inlineSyncResFile (read : SyncRead) (rf : RegFileBase) k (a : EActionT k) : EActionT k :=
    match rf with
    | @Build_RegFileBase _isWrMask _num _dataArray _readers _write _idxNum _Data _init =>
      match read with
      | @Build_SyncRead _readReqName _readResName _readRegName =>
        match _readers with
        | Async _ => a
        | Sync isAddr reads =>
          match (existsb (SyncRead_eqb read) reads) with
          | true =>
            match a with
            | EMCall g sign arg cont =>
              match String.eqb _readResName g with
              | true =>
                match Signature_dec sign (Void, Array _num _Data) with
                | left isEq =>
                  ESyncReadRes _idxNum _readResName _readRegName _dataArray _write _isWrMask isAddr (fun array => inlineSyncResFile read rf (match isEq in _ = Y return fullType ty (SyntaxKind (snd Y)) -> EActionT k with | eq_refl => cont end array))
                | right _ => EMCall g sign arg (fun ret => inlineSyncResFile read rf (cont ret))
                end
              | false => EMCall g sign arg (fun ret => inlineSyncResFile read rf (cont ret))
              end
            | ELetExpr _ e cont => ELetExpr e (fun ret => inlineSyncResFile read rf (cont ret))
            | ELetAction _ a cont => ELetAction (inlineSyncResFile read rf a) (fun ret => inlineSyncResFile read rf (cont ret))
            | EReadNondet k c => EReadNondet k (fun ret => inlineSyncResFile read rf (c ret))
            | EReadReg r k c => EReadReg r k (fun ret => inlineSyncResFile read rf (c ret))
            | EWriteReg r k e a => EWriteReg r e (inlineSyncResFile read rf a)
            | EIfElse p _ aT aF c => EIfElse p (inlineSyncResFile read rf aT) (inlineSyncResFile read rf aF) (fun ret => inlineSyncResFile read rf (c ret))
            | ESys ls c => ESys ls (inlineSyncResFile read rf c)
            | EReturn e => EReturn e
            | EAsyncRead idxNum num readPort dataArray writePort isWriteMask idx k cont =>
              EAsyncRead idxNum readPort dataArray writePort isWriteMask idx (fun ret => inlineSyncResFile read rf (cont ret))
            | EWrite idxNum num writePort dataArray idx Data val mask cont =>
              EWrite idxNum writePort dataArray idx val mask (inlineSyncResFile read rf cont)
            | ESyncReadReq idxNum num readReq readReg dataArray idx Data isAddr cont =>
              ESyncReadReq idxNum num readReq readReg dataArray idx Data isAddr (inlineSyncResFile read rf cont)
            | ESyncReadRes idxNum num readResp readReg dataArray writePort isWriteMask Data isAddr cont =>
              ESyncReadRes idxNum readResp readReg dataArray writePort isWriteMask isAddr (fun v => inlineSyncResFile read rf (cont v))
            end
          | false => a
          end
        end
      end
    end.

  Fixpoint inlineSyncReqFile (read : SyncRead) (rf : RegFileBase) k (a : EActionT k) : EActionT k :=
    match rf with
    | @Build_RegFileBase _isWrMask _num _dataArray _readers _write _idxNum _Data _init =>
      match read with
      | @Build_SyncRead _readReqName _readResName _readRegName =>
        match _readers with
        | Async _ => a
        | Sync isAddr reads =>
          match (existsb (SyncRead_eqb read) reads) with
          | true =>
            match a with
            | EMCall g sign arg cont =>
              match String.eqb _readReqName g with
              | true =>
                match Signature_dec sign (Bit (Nat.log2_up _idxNum), Void) with
                | left isEq =>
                  let inValue := (match isEq in _ = Y return Expr ty (SyntaxKind (fst Y)) with | eq_refl => arg end) in
                  ELetExpr ($$ WO)%kami_expr
                           (fun v => ESyncReadReq _idxNum _num _readReqName _readRegName _dataArray inValue _Data isAddr (inlineSyncReqFile read rf (match isEq in _ = Y return fullType ty (SyntaxKind (snd Y)) -> EActionT k with
                                                                                | eq_refl => cont
                                                                                end v)))
                | right _ => EMCall g sign arg (fun ret => inlineSyncReqFile read rf (cont ret))
                end
              | false => EMCall g sign arg (fun ret => inlineSyncReqFile read rf (cont ret))
              end
            | ELetExpr _ e cont => ELetExpr e (fun ret => inlineSyncReqFile read rf (cont ret))
            | ELetAction _ a cont => ELetAction (inlineSyncReqFile read rf a) (fun ret => inlineSyncReqFile read rf (cont ret))
            | EReadNondet k c => EReadNondet k (fun ret => inlineSyncReqFile read rf (c ret))
            | EReadReg r k c => EReadReg r k (fun ret => inlineSyncReqFile read rf (c ret))
            | EWriteReg r k e a => EWriteReg r e (inlineSyncReqFile read rf a)
            | EIfElse p _ aT aF c => EIfElse p (inlineSyncReqFile read rf aT) (inlineSyncReqFile read rf aF) (fun ret => inlineSyncReqFile read rf (c ret))
            | ESys ls c => ESys ls (inlineSyncReqFile read rf c)
            | EReturn e => EReturn e
            | EAsyncRead idxNum num readPort dataArray writePort isWriteMask idx k cont =>
              EAsyncRead idxNum readPort dataArray writePort isWriteMask idx (fun ret => inlineSyncReqFile read rf (cont ret))
            | EWrite idxNum num writePort dataArray idx Data val mask cont =>
              EWrite idxNum writePort dataArray idx val mask (inlineSyncReqFile read rf cont)
            | ESyncReadReq idxNum num readReq readReg dataArray idx Data isAddr cont =>
              ESyncReadReq idxNum num readReq readReg dataArray idx Data isAddr (inlineSyncReqFile read rf cont)
            | ESyncReadRes idxNum num readResp readReg dataArray writePort isWriteMask Data isAddr cont =>
              ESyncReadRes idxNum readResp readReg dataArray writePort isWriteMask isAddr (fun v => inlineSyncReqFile read rf (cont v))
            end
          | false => a
          end
        end
      end
    end.

  End ReadMap.

    Definition getRegFileWrite (rf : RegFileBase) : DefMethT :=
      match rf with
      | @Build_RegFileBase isWrMask num dataArray _ write idxNum Data _ =>
        writeRegFileFn isWrMask num dataArray write idxNum Data
      end.

    Definition getAsyncReads (rf : RegFileBase) (read : string) : DefMethT :=
      (read,
       existT MethodT (Bit (Nat.log2_up (rfIdxNum rf)), Array (rfNum rf) (rfData rf))
              (buildNumDataArray (rfNum rf) (rfDataArray rf) (rfIdxNum rf) (rfData rf))).

    Definition getSyncReq (rf : RegFileBase) (isAddr : bool) (read : SyncRead) : DefMethT :=
      if isAddr
      then
        (readReqName read,
         existT MethodT (Bit (Nat.log2_up (rfIdxNum rf)), Void)
                (fun (ty : Kind -> Type) (idx : fullType ty (SyntaxKind (fst (Bit (Nat.log2_up (rfIdxNum rf)), Void)))) =>
                   (Write readRegName read : fst (Bit (Nat.log2_up (rfIdxNum rf)), Void) <-
                                                 Var ty (SyntaxKind (fst (Bit (Nat.log2_up (rfIdxNum rf)), Void))) idx; Ret
                                                                                Const ty WO)%kami_action))
      else
        (readReqName read,
         existT MethodT (Bit (Nat.log2_up (rfIdxNum rf)), Void)
                (fun (ty : Kind -> Type) (idx : fullType ty (SyntaxKind (fst (Bit (Nat.log2_up (rfIdxNum rf)), Void)))) =>
                   (LETA vals : Array (rfNum rf) (rfData rf) <- buildNumDataArray (rfNum rf) (rfDataArray rf) (rfIdxNum rf) (rfData rf) ty idx;
                      Write readRegName read : Array (rfNum rf) (rfData rf) <- Var ty (SyntaxKind (Array (rfNum rf) (rfData rf))) vals;
                      Ret Const ty WO)%kami_action)).

    Definition getSyncRes (rf : RegFileBase) (isAddr : bool) (read : SyncRead) : DefMethT :=
      if isAddr
      then
        (readResName read,
         existT MethodT (Void, Array (rfNum rf) (rfData rf))
                (fun (ty : Kind -> Type) (_ : fullType ty (SyntaxKind (fst (Void, Array (rfNum rf) (rfData rf))))) =>
                   (Read name : Bit (Nat.log2_up (rfIdxNum rf)) <- readRegName read;
                      buildNumDataArray (rfNum rf) (rfDataArray rf) (rfIdxNum rf) (rfData rf) ty name)%kami_action))
      else
        (readResName read,
         existT MethodT (Void, Array (rfNum rf) (rfData rf))
                (fun (ty : Kind -> Type) (_ : fullType ty (SyntaxKind (fst (Void, Array (rfNum rf) (rfData rf))))) =>
                   (Read data : Array (rfNum rf) (rfData rf) <- readRegName read;
                      Ret Var ty (SyntaxKind (Array (rfNum rf) (rfData rf))) data)%kami_action)).

    Definition inlineSingle_Flat_pos meths1 meths2 n :=
      match nth_error meths1 n with
      | Some f => map (inlineSingle_Meth f) meths2
      | None => meths2
      end.

    Definition inlineSingle_pos k meths (a : ActionT ty k) n :=
      match nth_error meths n with
      | Some f => inlineSingle a f
      | None => a
      end.

    Definition getEachRfMethod (rf : RegFileBase) : list DefMethT :=
      (getRegFileWrite rf :: match (rfRead rf) with
                             | Async read => map (getAsyncReads rf) read
                             | Sync isAddr read => map (getSyncReq rf isAddr) read
                                                       ++ map (getSyncRes rf isAddr) read
                             end).

    Definition EgetRegFileMapMethods k (rf : RegFileBase) : list (EActionT k -> EActionT k) :=
      (inlineWriteFile rf :: match (rfRead rf) with
                             | Async read => map (fun x => @inlineAsyncReadFile x rf k) read
                             | Sync isAddr read => map (fun x => @inlineSyncReqFile x rf k) read
                                                       ++ map (fun x => @inlineSyncResFile x rf k) read
                             end).

    Definition EeachRfMethodInliners k (lrf : list RegFileBase) : list (EActionT k -> EActionT k) :=
      concat (map (fun rf => EgetRegFileMapMethods k rf) lrf).

    Definition eachRfMethodInliners k (lrf : list RegFileBase) : list (ActionT ty k -> ActionT ty k) :=
      (concat (map (fun rf => (map (fun f a' => @inlineSingle ty k a' f) (getRegFileMethods rf))) lrf)).

    Definition apply_nth {A : Type} (lf : list (A -> A)) (a : A) (n : nat) :=
      match nth_error lf n with
      | Some f => f a
      | None => a
      end.

    Definition preCompileRegFiles k (ea : EActionT k) (lrf : list RegFileBase) : EActionT k :=
      fold_left (apply_nth (EeachRfMethodInliners k lrf)) (seq 0 (length (EeachRfMethodInliners k lrf))) ea.

    Definition compileActions (readMap : regMapTy) (acts: list (ActionT ty Void)) :=
      fold_left (fun acc a =>
                   CompLetFull acc (fun _ writeMap =>
                                      (CompLetFull (CompRet ($$ WO)%kami_expr
                                                            (CompactRegMap (VarRegMap writeMap)))
                                      (fun _ v => @compileAction v _ a ($$ true)%kami_expr (VarRegMap v))))) acts
                (CompRet ($$ WO)%kami_expr (VarRegMap readMap)).

    Definition compileActionsRf (readMap : regMapTy) (acts : list (ActionT ty Void)) (lrf : list RegFileBase) :=
      fold_left (fun acc a =>
                   CompLetFull acc (fun _ writeMap =>
                                      (CompLetFull (CompRet ($$ WO)%kami_expr
                                                            (CompactRegMap (VarRegMap writeMap)))
                                                   (fun _ v => @EcompileAction v _ (preCompileRegFiles (Action_EAction a) lrf) ($$ true)%kami_expr (VarRegMap v))))) acts
                (CompRet ($$ WO)%kami_expr (VarRegMap readMap)).

    Definition compileRules (readMap : regMapTy) (rules: list RuleT) :=
      compileActions readMap (map (fun a => snd a ty) rules).

    Definition compileRulesRf (readMap : regMapTy) (rules : list RuleT) (lrf : list RegFileBase) :=
      compileActionsRf readMap (map (fun a => snd a ty) rules) lrf.

End Compile.

Section Semantics.
  Local Notation UpdRegT := RegsT.
  Local Notation UpdRegsT := (list UpdRegT).

  Local Notation RegMapType := (RegsT * UpdRegsT)%type.

  Section PriorityUpds.

    Variable o: RegsT.
    Inductive PriorityUpds: UpdRegsT -> RegsT -> Prop :=
    | NoUpds: PriorityUpds nil o
    | ConsUpds (prevUpds: UpdRegsT) (prevRegs: RegsT)
               (prevCorrect: PriorityUpds prevUpds prevRegs)
               (u: UpdRegT)
               (curr: RegsT)
               (currRegsTCurr: getKindAttr o = getKindAttr curr)
               (Hcurr: forall s v, In (s, v) curr -> In (s, v) u \/ ((~ In s (map fst u)) /\ In (s, v) prevRegs))
               fullU
               (HFullU: fullU = u :: prevUpds):
        PriorityUpds fullU curr.

    Lemma prevPrevRegsTrue prevUpds:
      forall prev, PriorityUpds prevUpds prev -> getKindAttr o = getKindAttr prev.
    Proof.
      induction 1; eauto.
    Qed.

  End PriorityUpds.

  Inductive SemRegMapExpr: (RegMapExpr type RegMapType) -> RegMapType -> Prop :=
  | SemVarRegMap v:
      SemRegMapExpr (VarRegMap _ v) v
  | SemUpdRegMapTrue r (pred: Bool @# type) k val regMap
                     (PredTrue: evalExpr pred = true)
                     old upds
                     (HSemRegMap: SemRegMapExpr regMap (old, upds))
                     upds'
                     (HEqual : upds' = (hd nil upds ++ ((r, existT _ k (evalExpr val)) :: nil)) :: tl upds):
      SemRegMapExpr (@UpdRegMap _ _ r pred k val regMap) (old, upds')
  | SemUpdRegMapFalse r (pred: Bool @# type) k val regMap
                      (PredTrue: evalExpr pred = false)
                      old upds
                      (HSemRegMap: SemRegMapExpr regMap (old, upds)):
      SemRegMapExpr (@UpdRegMap _ _ r pred k val regMap) (old, upds)
  | SemCompactRegMap old upds regMap (HSemRegMap: SemRegMapExpr regMap (old, upds)):
      SemRegMapExpr (@CompactRegMap _ _ regMap) (old, nil::upds).

  Definition WfRegMapExpr (regMapExpr : RegMapExpr type RegMapType) (regMap : RegMapType) :=
    SemRegMapExpr regMapExpr regMap /\
    let '(old, new) := regMap in
    forall u, In u new -> NoDup (map fst u) /\ SubList (getKindAttr u) (getKindAttr old).

  Inductive SemCompActionT: forall k, CompActionT type RegMapType k -> RegMapType ->  MethsT -> type k -> Prop :=
  | SemCompCallTrue (f: string) (argRetK: Kind * Kind) (pred: Bool @# type)
             (arg: fst argRetK @# type)
             lret (cont: fullType type (SyntaxKind (snd argRetK)) -> CompActionT _ _ lret)
             (ret: fullType type (SyntaxKind (snd argRetK)))
             regMap calls val newCalls
             (HNewCalls : newCalls = (f, existT _ argRetK (evalExpr arg, ret)) :: calls)
             (HSemCompActionT: SemCompActionT (cont ret) regMap calls val)
             (HPred : evalExpr pred = true):
      SemCompActionT (@CompCall _ _ f argRetK pred arg lret cont) regMap newCalls val
  | SemCompCallFalse (f: string) (argRetK: Kind * Kind) (pred: Bool @# type)
             (arg: fst argRetK @# type)
             lret (cont: fullType type (SyntaxKind (snd argRetK)) -> CompActionT _ _ lret)
             (ret: fullType type (SyntaxKind (snd argRetK)))
             regMap calls val
             (HSemCompActionT: SemCompActionT (cont ret) regMap calls val)
             (HPred : evalExpr pred = false):
      SemCompActionT (@CompCall _ _ f argRetK pred arg lret cont) regMap calls val
  | SemCompLetExpr k e lret cont
                   regMap calls val
                   (HSemCompActionT: SemCompActionT (cont (evalExpr e)) regMap calls val):
      SemCompActionT (@CompLetExpr _ _ k e lret cont) regMap calls val
  | SemCompNondet k lret cont
                  ret regMap calls val
                  (HSemCompActionT: SemCompActionT (cont ret) regMap calls val):
      SemCompActionT (@CompNondet _ _ k lret cont) regMap calls val
  | SemCompSys pred ls lret cont
               regMap calls val
               (HSemCompActionT: SemCompActionT cont regMap calls val):
      SemCompActionT (@CompSys _ _ pred ls lret cont) regMap calls val
  | SemCompRead r k readMap lret cont
                regMap calls val regVal
                updatedRegs readMapValOld readMapValUpds
                (HReadMap: SemRegMapExpr readMap (readMapValOld, readMapValUpds))
                (HUpdatedRegs: PriorityUpds readMapValOld readMapValUpds updatedRegs)
                (HIn: In (r, (existT _ k regVal)) updatedRegs)
                (HSemCompActionT: SemCompActionT (cont regVal) regMap calls val):
      SemCompActionT (@CompRead _ _ r k readMap lret cont) regMap calls val
  | SemCompRet lret e regMap regMapVal calls
               (HCallsNil : calls = nil)
               (HRegMapWf: WfRegMapExpr regMap regMapVal):
      SemCompActionT (@CompRet _ _ lret e regMap) regMapVal calls (evalExpr e)
  | SemCompLetFull k a lret cont
                   regMap_a calls_a val_a
                   (HSemCompActionT_a: SemCompActionT a regMap_a calls_a val_a)
                   regMap_cont calls_cont val_cont newCalls
                   (HNewCalls : newCalls = calls_a ++ calls_cont)
                   (HSemCompActionT_cont: SemCompActionT (cont val_a regMap_a) regMap_cont calls_cont val_cont):
      SemCompActionT (@CompLetFull _ _ k a lret cont) regMap_cont newCalls val_cont
  | SemCompAsyncRead num (readPort dataArray writePort: string) isWriteMask idxNum (idx : Bit (Nat.log2_up idxNum) @# type) pred Data readMap lret
                     updatedRegs readMapValOld readMapValUpds regVal writeMap writeMapTy regMap
                     (HWriteMap: SemRegMapExpr writeMap writeMapTy)
                     (HReadMap : SemRegMapExpr readMap (readMapValOld, readMapValUpds))
                     (HUpdatedRegs : PriorityUpds readMapValOld readMapValUpds updatedRegs)
                     (HIn :  In (dataArray, (existT _ (SyntaxKind (Array idxNum Data)) regVal)) updatedRegs)
                     cont calls val contArray
                     (HContArray : contArray =
                                   BuildArray (fun i : Fin.t num =>
                                                 ReadArray
                                                   (Var type _ regVal)
                                                   (CABit Add (Var type (SyntaxKind _) (evalExpr idx) ::
                                                                   Const type (natToWord _ (proj1_sig (Fin.to_nat i)))::nil))))
                     (HSemCompActionT : SemCompActionT (cont (evalExpr contArray) writeMapTy) regMap calls val):
      SemCompActionT (@CompAsyncRead _ _  idxNum num readPort dataArray writePort isWriteMask idx pred Data writeMap readMap lret cont) regMap calls val
  | SemCompWriteSome num (writePort dataArray : string) idxNum (idx  : Bit (Nat.log2_up idxNum) @# type) Data (array : Array num Data @# type)
                     (optMask : option (Array num Bool @# type)) (writeMap readMap : RegMapExpr type RegMapType) lret mask
                     (HMask : optMask = Some mask)
                     updatedRegs readMapValOld readMapValUpds regVal
                     (HReadMap : SemRegMapExpr readMap (readMapValOld, readMapValUpds))
                     (HUpdatedRegs : PriorityUpds readMapValOld readMapValUpds updatedRegs)
                     (HIn : In (dataArray, (existT _ (SyntaxKind (Array idxNum Data)) regVal)) updatedRegs)
                     regMapVal pred
                     (HUpdate : WfRegMapExpr (UpdRegMap dataArray pred
                                                        (fold_left (fun newArr i =>
                                                                      ITE
                                                                        (ReadArrayConst mask i)
                                                                        (UpdateArray newArr
                                                                                (CABit Add (idx :: Const type (natToWord _ (proj1_sig (Fin.to_nat i)))
                                                                                :: nil))
                                                                                (ReadArrayConst array i))
                                                                        newArr
                                                                   ) (getFins num)
                                                                   (Var type (SyntaxKind (Array idxNum Data)) regVal))
                                                        writeMap) regMapVal)
                     cont regMap_cont calls val
                     (HSemCompActionT : SemCompActionT (cont regMapVal) regMap_cont calls val):
      SemCompActionT (@CompWrite _ _ idxNum num writePort dataArray idx Data array optMask pred writeMap readMap lret cont) regMap_cont calls val
  | SemCompWriteNone num (writePort dataArray : string) idxNum (idx  : Bit (Nat.log2_up idxNum) @# type) Data (array : Array num Data @# type)
                     (optMask : option (Array num Bool @# type)) (writeMap readMap : RegMapExpr type RegMapType) lret
                     (HMask : optMask = None)
                     updatedRegs readMapValOld readMapValUpds regVal
                     (HReadMap : SemRegMapExpr readMap (readMapValOld, readMapValUpds))
                     (HUpdatedRegs : PriorityUpds readMapValOld readMapValUpds updatedRegs)
                     (HIn : In (dataArray, (existT _ (SyntaxKind (Array idxNum Data)) regVal)) updatedRegs)
                     regMapVal pred
                     (HUpdate : WfRegMapExpr (UpdRegMap dataArray pred
                                                        (fold_left (fun newArr i =>
                                                                      (UpdateArray newArr
                                                                                (CABit Add (idx :: Const type (natToWord _ (proj1_sig (Fin.to_nat i)))
                                                                                :: nil))
                                                                                (ReadArrayConst array i))
                                                                   ) (getFins num)
                                                                   (Var type (SyntaxKind (Array idxNum Data)) regVal))
                                                        writeMap) regMapVal)
                     cont regMap_cont calls val
                     (HSemCompActionT : SemCompActionT (cont regMapVal) regMap_cont calls val):
      SemCompActionT (@CompWrite _ _ idxNum num writePort dataArray idx Data array optMask pred writeMap readMap lret cont) regMap_cont calls val
  | SemCompSyncReadReqTrue num idxNum readReqName readRegName dataArray (idx : Bit (Nat.log2_up idxNum) @# type) k (isAddr : bool)
                           (writeMap : RegMapExpr type RegMapType) readMap lret cont
                           regMapVal pred
                           (HisAddr : isAddr = true)
                           (HWriteMap : WfRegMapExpr (UpdRegMap readRegName pred (Var type (SyntaxKind _) (evalExpr idx)) writeMap) regMapVal)
                           regMap_cont calls val
                           (HSemCompActionT : SemCompActionT (cont regMapVal) regMap_cont calls val):
      SemCompActionT (@CompSyncReadReq _ _ idxNum num readReqName readRegName dataArray idx k isAddr pred writeMap readMap lret cont) regMap_cont calls val
  | SemCompSyncReadReqFalse num idxNum readReqName readRegName dataArray (idx : Bit (Nat.log2_up idxNum) @# type) Data (isAddr : bool)
                            (writeMap : RegMapExpr type RegMapType) readMap lret cont
                            regMapVal pred
                            (HisAddr : isAddr = false)
                            updatedRegs readMapValOld readMapValUpds regV
                            (HReadMap : SemRegMapExpr readMap (readMapValOld, readMapValUpds))
                            (HUpdatedRegs : PriorityUpds readMapValOld readMapValUpds updatedRegs)
                            (HRegVal : In (dataArray, (existT _ (SyntaxKind (Array idxNum Data)) regV)) updatedRegs)
                            (HWriteMap : WfRegMapExpr
                                           (UpdRegMap readRegName pred
                                                      (BuildArray (fun i : Fin.t num =>
                                                                     ReadArray
                                                                       (Var type _ regV)
                                                                       (CABit Add (Var type (SyntaxKind _) (evalExpr idx) ::
                                                                                Const type (natToWord _ (proj1_sig (Fin.to_nat i)))::nil)))) writeMap) regMapVal)
                            regMap_cont calls val
                            (HSemCompActionT : SemCompActionT (cont regMapVal) regMap_cont calls val):
      SemCompActionT (@CompSyncReadReq _ _ idxNum num readReqName readRegName dataArray idx Data isAddr pred writeMap readMap lret cont) regMap_cont calls val
  | SemCompSyncReadResTrue num idxNum readRespName readRegName dataArray writePort isWriteMask Data isAddr writeMap readMap lret cont
                           (HisAddr : isAddr = true)
                           writeMapTy
                           updatedRegs readMapValOld readMapValUpds regVal idx
                           (HWriteMap: SemRegMapExpr writeMap writeMapTy)
                           (HReadMap : SemRegMapExpr readMap (readMapValOld, readMapValUpds))
                           (HUpdatedRegs : PriorityUpds readMapValOld readMapValUpds updatedRegs)
                           (HRegVal1 : In (readRegName, existT _ (SyntaxKind (Bit (Nat.log2_up idxNum))) idx) updatedRegs)
                           (HRegVal2 : In (dataArray, existT _ (SyntaxKind (Array idxNum Data)) regVal) updatedRegs)
                           (contArray : Expr type (SyntaxKind (Array num Data)))
                           (HContArray : contArray =
                                         BuildArray (fun i : Fin.t num =>
                                                       ReadArray
                                                         (Var type _ regVal)
                                                         (CABit Add (Var type (SyntaxKind _) idx ::
                                                                         Const type (natToWord _ (proj1_sig (Fin.to_nat i)))::nil))))
                           regMap calls val
                           (HSemCompActionT : SemCompActionT (cont (evalExpr contArray) writeMapTy) regMap calls val):
      SemCompActionT (@CompSyncReadRes _ _ idxNum num readRespName readRegName dataArray writePort isWriteMask Data isAddr writeMap readMap lret cont) regMap calls val
  | SemCompSyncReadResFalse num idxNum readRespName readRegName dataArray writePort isWriteMask Data isAddr writeMap writeMapTy readMap lret cont
                            (HisAddr : isAddr = false)
                            updatedRegs readMapValOld readMapValUpds regVal
                            (HWriteMap: SemRegMapExpr writeMap writeMapTy)
                            (HReadMap : SemRegMapExpr readMap (readMapValOld, readMapValUpds))
                            (HUpdatedRegs : PriorityUpds readMapValOld readMapValUpds updatedRegs)
                            (HIn1 : In (readRegName, (existT _ (SyntaxKind (Array num Data)) regVal)) updatedRegs)
                            regMap calls val
                            (HSemCompActionT : SemCompActionT (cont regVal writeMapTy) regMap calls val):
      SemCompActionT (@CompSyncReadRes _ _ idxNum num readRespName readRegName dataArray writePort isWriteMask Data isAddr writeMap readMap lret cont) regMap calls val.

  Variable (k : Kind) (a : CompActionT type RegMapType k) (regInits : list RegInitT).

  Section Loop.
    Variable f: RegsT -> CompActionT type RegMapType Void.

    Inductive SemCompTrace: RegsT -> list UpdRegsT -> list MethsT -> Prop :=
    | SemCompTraceInit (oInit : RegsT) (lupds : list UpdRegsT) (lcalls : list MethsT)
                       (HNoUpds : lupds = nil) (HNoCalls : lcalls = nil)
                       (HInitRegs : Forall2 regInit oInit regInits) :
        SemCompTrace oInit lupds lcalls
    | SemCompTraceCont (o o' : RegsT) (lupds lupds' : list UpdRegsT) (upds : UpdRegsT)
                       (lcalls lcalls' : list MethsT) (calls : MethsT) val
                       (HOldTrace : SemCompTrace o lupds lcalls)
                       (HSemAction : SemCompActionT (f o) (o, upds) calls val)
                       (HNewUpds : lupds' = upds :: lupds)
                       (HNewCalls : lcalls' = calls :: lcalls)
                       (HPriorityUpds : PriorityUpds o upds o') :
        SemCompTrace o' lupds' lcalls'.
  End Loop.
End Semantics.

Section EActionT_Semantics.
  Variable o : RegsT.

  Inductive UpdOrMeth : Type :=
  | UmUpd : RegT -> UpdOrMeth
  | UmMeth : MethT -> UpdOrMeth.

  Definition UpdOrMeths := list UpdOrMeth.

  Fixpoint UpdOrMeths_RegsT (uml : UpdOrMeths) : RegsT :=
    match uml with
    | um :: uml' =>
      match um with
      | UmUpd u => u :: (UpdOrMeths_RegsT uml')
      | UmMeth _ => (UpdOrMeths_RegsT uml')
      end
    | nil => nil
    end.

  Fixpoint UpdOrMeths_MethsT (uml : UpdOrMeths) : MethsT :=
    match uml with
    | um :: uml' =>
      match um with
      | UmUpd _ => (UpdOrMeths_MethsT uml')
      | UmMeth m => m :: (UpdOrMeths_MethsT uml')
      end
    | nil => nil
    end.

  Inductive ESemAction :
    forall k, EActionT type k -> UpdOrMeths -> type k -> Prop :=
  | ESemCall (meth : string) (s : Kind * Kind) (marg : Expr type (SyntaxKind (fst s))) (mret : type (snd s)) (retK : Kind)
             (fret : type retK) (cont : type (snd s) -> EActionT type retK) (uml : UpdOrMeths) (auml : list UpdOrMeth)
             (HNewList : auml = (UmMeth (meth, existT SignT s (evalExpr marg, mret)) :: uml))
             (HESemAction : ESemAction (cont mret) uml fret) :
      ESemAction (EMCall meth s marg cont) auml fret
  | ESemLetExpr (k : FullKind) (e : Expr type k) (retK : Kind) (fret : type retK) (cont : fullType type k -> EActionT type retK)
                (uml : UpdOrMeths) (HESemAction : ESemAction (cont (evalExpr e)) uml fret) :
      ESemAction (ELetExpr e cont) uml fret
  | ESemLetAction (k : Kind) (ea : EActionT type k) (v : type k) (retK : Kind) (fret : type retK) (cont : type k -> EActionT type retK)
                  (newUml : list UpdOrMeth) (newUmlCont : list UpdOrMeth)
                  (HDisjRegs : DisjKey (UpdOrMeths_RegsT newUml) (UpdOrMeths_RegsT newUmlCont)) (HESemAction : ESemAction ea newUml v)
                  (HESemActionCont : ESemAction (cont v) newUmlCont fret)
                  (uNewUml : UpdOrMeths)
                  (HNewUml : uNewUml = newUml ++ newUmlCont) :
      ESemAction (ELetAction ea cont) uNewUml fret
  | ESemReadNondet (valueT : FullKind) (valueV : fullType type valueT) (retK : Kind) (fret : type retK)
                   (cont : fullType type valueT -> EActionT type retK) (newUml : UpdOrMeths)
                   (HESemAction : ESemAction (cont valueV) newUml fret):
      ESemAction (EReadNondet _ cont) newUml fret
  | ESemReadReg (r : string) (regT : FullKind) (regV : fullType type regT) (retK : Kind) (fret : type retK) (cont : fullType type regT -> EActionT type retK)
                (newUml : UpdOrMeths) (HRegVal : In (r, existT _ regT regV) o)
                (HESemAction : ESemAction (cont regV) newUml fret) :
      ESemAction (EReadReg r _ cont) newUml fret
  | ESemWriteReg (r : string) (k : FullKind) (e : Expr type k) (retK : Kind) (fret : type retK) (cont : EActionT type retK)
                 (newUml : list UpdOrMeth) (anewUml : list UpdOrMeth)
                 (HRegVal : In (r, k) (getKindAttr o))
                 (HDisjRegs : key_not_In r (UpdOrMeths_RegsT newUml))
                 (HANewUml : anewUml = (UmUpd (r, existT _ _ (evalExpr e))) :: newUml)
                 (HESemAction : ESemAction cont newUml fret):
      ESemAction (EWriteReg r e cont) anewUml fret
  | ESemIfElseTrue (p : Expr type (SyntaxKind Bool)) (k1 : Kind) (ea ea' : EActionT type k1) (r1 : type k1) (k2 : Kind) (cont : type k1 -> EActionT type k2)
                   (newUml1 newUml2 : list UpdOrMeth) (r2 : type k2)
                   (HDisjRegs : DisjKey (UpdOrMeths_RegsT newUml1) (UpdOrMeths_RegsT newUml2))
                   (HTrue : evalExpr p = true)
                   (HEAction : ESemAction ea  newUml1 r1)
                   (HESemAction : ESemAction (cont r1) newUml2 r2)
                   (unewUml : UpdOrMeths)
                   (HUNewUml : unewUml = newUml1 ++ newUml2) :
      ESemAction (EIfElse p ea ea' cont) unewUml r2
  | ESemIfElseFalse (p : Expr type (SyntaxKind Bool)) (k1 : Kind) (ea ea' : EActionT type k1) (r1 : type k1) (k2 : Kind) (cont : type k1 -> EActionT type k2)
                    (newUml1 newUml2 : list UpdOrMeth) (r2 : type k2)
                    (HDisjRegs : DisjKey (UpdOrMeths_RegsT newUml1) (UpdOrMeths_RegsT newUml2))
                    (HFalse : evalExpr p = false)
                    (HEAction : ESemAction ea' newUml1 r1)
                    (HESemAction : ESemAction (cont r1) newUml2 r2)
                    (unewUml : UpdOrMeths)
                    (HUNewUml : unewUml = newUml1 ++ newUml2) :
      ESemAction (EIfElse p ea ea' cont) unewUml r2
  | ESemSys (ls : list (SysT type)) (k : Kind) (cont : EActionT type k) (r : type k) (newUml : UpdOrMeths)
            (HESemAction : ESemAction cont newUml r) :
      ESemAction (ESys ls cont) newUml r
  | ESemReturn (k : Kind) (e : Expr type (SyntaxKind k)) (evale : fullType type (SyntaxKind k))
               (HEvalE : evale = evalExpr e)
               (newUml : UpdOrMeths)
               (HNewUml : newUml = nil) :
      ESemAction (EReturn e) newUml evale
  | ESemAsyncRead (idxNum num : nat) (readPort dataArray : string) writePort isWriteMask (idx : Bit (Nat.log2_up idxNum) @# type) (Data : Kind) (retK : Kind) (fret : type retK)
                  (newUml : UpdOrMeths) (regV : fullType type (SyntaxKind (Array idxNum Data)))
                  (HRegVal : In (dataArray, (existT _ (SyntaxKind (Array idxNum Data)) regV)) o)
                  (cont : type (Array num Data) -> EActionT type retK)
                  (contArray : Expr type (SyntaxKind (Array num Data)))
                  (HContArray : contArray =
                                BuildArray (fun i : Fin.t num =>
                                              ReadArray
                                                (Var type _ regV)
                                                (CABit Add (Var type (SyntaxKind _) (evalExpr idx) ::
                                                                Const type (natToWord _ (proj1_sig (Fin.to_nat i)))::nil))))
                  (HESemAction : ESemAction (cont (evalExpr contArray)) newUml fret):
      ESemAction (EAsyncRead idxNum num readPort dataArray writePort isWriteMask idx Data cont) newUml fret
  | ESemWriteSome (idxNum num : nat) (writePort dataArray : string) (idx : Bit (Nat.log2_up idxNum) @# type) (Data : Kind) (array : Array num Data @# type)
                  (optMask : option (Array num Bool @# type)) (retK : Kind) (fret : type retK) (cont : EActionT type retK) (newUml : UpdOrMeths)
                  (anewUml : list UpdOrMeth) (regV : fullType type (SyntaxKind (Array idxNum Data))) (mask : Array num Bool @# type)
                  (HRegVal : In (dataArray, (existT _ (SyntaxKind (Array idxNum Data)) regV)) o)
                  (HMask : optMask = Some mask)
                  (HANewUml : anewUml =
                              (UmUpd (dataArray, existT _ _
                                                      (evalExpr (fold_left (fun newArr i =>
                                                                      ITE
                                                                        (ReadArrayConst mask i)
                                                                        (UpdateArray newArr
                                                                                (CABit Add (idx :: Const type (natToWord _ (proj1_sig (Fin.to_nat i)))
                                                                                :: nil))
                                                                                (ReadArrayConst array i))
                                                                        newArr
                                                                           ) (getFins num)
                                                                           (Var type (SyntaxKind (Array idxNum Data)) regV))))) :: newUml)
                  (HDisjRegs : key_not_In dataArray (UpdOrMeths_RegsT newUml))
                  (HESemAction : ESemAction cont newUml fret) :
      ESemAction (EWrite idxNum writePort dataArray idx array optMask cont) anewUml fret
  | ESemWriteNone (idxNum num : nat) (writePort dataArray : string) (idx : Bit (Nat.log2_up idxNum) @# type) (Data : Kind) (array : Array num Data @# type)
                  (optMask : option (Array num Bool @# type)) (retK : Kind) (fret : type retK) (cont : EActionT type retK) (newUml : UpdOrMeths)
                  (anewUml : list UpdOrMeth) (regV : fullType type (SyntaxKind (Array idxNum Data)))
                  (HRegVal : In (dataArray, (existT _ (SyntaxKind (Array idxNum Data)) regV)) o)
                  (HMask : optMask = None)
                  (HANewUml : anewUml =
                              (UmUpd (dataArray, existT _ _
                                                      (evalExpr (fold_left (fun newArr i =>
                                                                      (UpdateArray newArr
                                                                                (CABit Add (idx :: Const type (natToWord _ (proj1_sig (Fin.to_nat i)))
                                                                                :: nil))
                                                                                (ReadArrayConst array i))
                                                                   ) (getFins num)
                                                                           (Var type (SyntaxKind (Array idxNum Data)) regV))))) :: newUml)
                  (HDisjRegs : key_not_In dataArray (UpdOrMeths_RegsT newUml))
                  (HESemAction : ESemAction cont newUml fret) :
      ESemAction (EWrite idxNum writePort dataArray idx array optMask cont) anewUml fret
  | ESemSyncReadReqTrue (idxNum num : nat) (readReqName readRegName dataArray : string) (idx : Bit (Nat.log2_up idxNum) @# type) (Data : Kind) (isAddr : bool)
                        (retK : Kind) (fret : type retK) (cont : EActionT type retK) (newUml : UpdOrMeths) (anewUml : list UpdOrMeth)
                        (HisAddr : isAddr = true)
                        (HRegVal : In (readRegName, (SyntaxKind (Bit (Nat.log2_up idxNum)))) (getKindAttr o))
                        (HDisjRegs : key_not_In readRegName (UpdOrMeths_RegsT newUml))
                        (HANewUml : anewUml = (UmUpd (readRegName, existT _ _ (evalExpr idx))) :: newUml)
                        (HESemAction : ESemAction cont newUml fret):
      ESemAction (ESyncReadReq idxNum num readReqName readRegName dataArray idx Data isAddr cont) anewUml fret
  | ESemSyncReadReqFalse (idxNum num : nat) (readReqName readRegName dataArray : string) (idx : Bit (Nat.log2_up idxNum) @# type) (Data : Kind) (isAddr : bool)
                         (retK : Kind) (fret : type retK) (cont : EActionT type retK) (newUml : UpdOrMeths) (anewUml : list UpdOrMeth)
                         (regV : fullType type (SyntaxKind (Array idxNum Data)))
                         (HisAddr : isAddr = false)
                         (HRegVal1 : In (readRegName, (SyntaxKind (Array num Data))) (getKindAttr o))
                         (HRegVal2 : In (dataArray, (existT _ (SyntaxKind (Array idxNum Data)) regV)) o)
                         (HDisjRegs : key_not_In readRegName (UpdOrMeths_RegsT newUml))
                         (HANewUml : anewUml =
                                     (UmUpd (readRegName, existT _ _
                                                               (evalExpr
                                                                  (BuildArray (fun i : Fin.t num =>
                                                     ReadArray
                                                       (Var type _ regV)
                                                       (CABit Add (Var type (SyntaxKind _) (evalExpr idx) ::
                                                                       Const type (natToWord _ (proj1_sig (Fin.to_nat i)))::nil))))))) :: newUml)
                         (HESemAction : ESemAction cont newUml fret):
      ESemAction (ESyncReadReq idxNum num readReqName readRegName dataArray idx Data isAddr cont) anewUml fret
  | ESemSyncReadResTrue (idxNum num : nat) (readRespName readRegName dataArray : string) writePort isWriteMask (Data : Kind) (isAddr : bool) (retK : Kind) (fret : type retK)
                        (regVal : fullType type (SyntaxKind (Array idxNum Data))) (idx : fullType type (SyntaxKind (Bit (Nat.log2_up idxNum))))
                        (cont : type (Array num Data) -> EActionT type retK)
                        (HisAddr : isAddr = true)
                        (HRegVal1 : In (readRegName, existT _ (SyntaxKind (Bit (Nat.log2_up idxNum))) idx) o)
                        (HRegVal2 : In (dataArray, existT _ (SyntaxKind (Array idxNum Data)) regVal) o)
                        (contArray : Expr type (SyntaxKind (Array num Data)))
                        (HContArray : contArray =
                                      BuildArray (fun i : Fin.t num =>
                                                       ReadArray
                                                         (Var type _ regVal)
                                                         (CABit Add (Var type (SyntaxKind _) idx ::
                                                                         Const type (natToWord _ (proj1_sig (Fin.to_nat i)))::nil))))
                        (newUml : UpdOrMeths)
                        (HESemAction : ESemAction (cont (evalExpr contArray)) newUml fret):
      ESemAction (ESyncReadRes idxNum num readRespName readRegName dataArray writePort isWriteMask Data isAddr cont)  newUml fret
  | ESemSyncReadResFalse (idxNum num : nat) (readRespName readRegName dataArray : string) writePort isWriteMask (Data : Kind) (isAddr : bool) (retK : Kind) (fret : type retK)
                         (regVal : fullType type (SyntaxKind (Array num Data))) (cont : type (Array num Data) -> EActionT type retK)
                         (HisAddr : isAddr = false)
                         (HRegVal : In (readRegName, existT _ (SyntaxKind (Array num Data)) regVal) o)
                         (newUml : UpdOrMeths)
                         (HESemAction : ESemAction (cont regVal) newUml fret):
      ESemAction (ESyncReadRes idxNum num readRespName readRegName dataArray writePort isWriteMask Data isAddr cont) newUml fret.

End EActionT_Semantics.

author: sifive

repo: Kami

save_path: github-repos/coq/sifive-Kami


text:
Require Export Iron.Language.SimplePCF.Base.

(********************************************************************)
(* Type Constructors *)
Inductive tycon : Type :=
 | TyConBool  : tycon
 | TyConNat   : tycon.
Hint Constructors tycon.

(* Type Expressions *)
Inductive ty  : Type :=
 | TCon       : tycon -> ty
 | TFun       : ty    -> ty -> ty.
Hint Constructors ty.

(* Baked-in Types *)
Definition tBool := TCon TyConBool.
Definition tNat  := TCon TyConNat.

(* Type Environments *)
Definition tyenv := list ty.

(********************************************************************)
(* Value Expressions *)
Inductive exp : Type :=
 (* Functions *)
 | XVar    : nat -> exp
 | XLam    : ty  -> exp -> exp
 | XApp    : exp -> exp -> exp

 (* Fixpoints *)
 | XFix    : ty  -> exp -> exp

 (* Naturals *)
 | XNat    : nat -> exp
 | XSucc   : exp -> exp
 | XPred   : exp -> exp

 (* Booleans *)
 | XTrue   : exp
 | XFalse  : exp
 | XIsZero : exp -> exp

 (* Branching *)
 | XIf     : exp -> exp -> exp -> exp.
Hint Constructors exp.

(* Weak normal forms.
   Expressions in weak normal form cannot be reduced further by
   call-by-value evaluation. *)
Inductive wnfX : exp -> Prop :=
 | Wnf_XVar
   :  forall i
   ,  wnfX (XVar i)

 | Wnf_XLam
   :  forall t1 x2
   ,  wnfX (XLam t1 x2)

 | Wnf_XNat
   :  forall n
   ,  wnfX (XNat n)

 | Wnf_XTrue
   :  wnfX XTrue

 | Wnf_False
   :  wnfX XFalse.
Hint Constructors wnfX.

(* Well formed expressions are closed under the given environment. *)
Fixpoint wfX (te: tyenv) (xx: exp) : Prop :=
 match xx with
 (* Functions *)
 | XVar i          => exists t, get i te = Some t
 | XLam t x        => wfX (te :> t) x
 | XApp x1 x2      => wfX te x1 /\ wfX te x2

 (* Fixpoints *)
 | XFix t x        => wfX (te :> t) x

 (* Naturals *)
 | XNat n          => True
 | XSucc x1        => wfX te x1
 | XPred x1        => wfX te x1

 (* Booleans *)
 | XTrue           => True
 | XFalse          => True
 | XIsZero x1      => wfX te x1

 (* Branching *)
 | XIf   x1 x2 x3  => wfX te x1 /\ wfX te x2 /\ wfX te x3
 end.

(* Closed expressions are well formed under an empty environment. *)
Definition closedX (xx: exp) : Prop
 := wfX nil xx.
Hint Unfold closedX.

(* Values are closed expressions that cannot be reduced further. *)
Definition value (x : exp)
 := wnfX x /\ closedX x.
Hint Unfold value.

Lemma value_wnfX
 : forall x, value x -> wnfX x.
Proof. intros. inverts H. auto. Qed.
Hint Resolve value_wnfX.

Lemma value_closedX
 : forall x, value x -> closedX x.
Proof. intros. inverts H. auto. Qed.
Hint Resolve value_closedX.

(********************************************************************)
(* Lifting of references to the environment.
   When we push new elements on the environment stack of an
   expression, we need to lift free indices in the expression
   across the new elements.

   For example given:
             t1, t0 |- 0 1 (\. 0 1 2) :: t3

   Pushing two more elements gives:
     t1, t0, ta, tb |- 2 3 (\. 0 3 4) :: t3
 *)
Fixpoint
 liftX  (d:  nat) (* current binding depth in expression *)
        (xx: exp) (* expression to lift *)
        : exp
 := match xx with
    |  XVar ix
    => if le_gt_dec d ix
        (* Index was referencing the env, so lift it across the new elem *)
        then XVar (S ix)
        (* Index was locally bound, so leave it be. *)
        else xx

    (* Increase the depth as we move across a lambda *)
    |  XLam t1 x1   => XLam t1 (liftX (S d) x1)
    |  XApp x1 x2   => XApp    (liftX d x1) (liftX d x2)

    (* Fixpoints *)
    |  XFix t1 x1   => XFix t1 (liftX (S d) x1)

    (* Naturals *)
    |  XNat _       => xx
    |  XSucc x1     => XSucc   (liftX d x1)
    |  XPred x1     => XPred   (liftX d x1)

    (* Booleans *)
    |  XTrue        => xx
    |  XFalse       => xx
    |  XIsZero x1   => XIsZero (liftX d x1)

    (* Branching *)
    |  XIf x1 x2 x3 => XIf (liftX d x1) (liftX d x2) (liftX d x3)
    end.

(********************************************************************)
(* Substitute for the outermost binder in an expression. *)
Fixpoint
 substX (d:  nat) (* current binding depth in expression *)
        (u:  exp) (* new expression to substitute *)
        (xx: exp) (* expression to substitute into *)
        : exp
 := match xx with
    (* Functions **********************)
    | XVar ix
    => match Nat.compare ix d with
       (* Index matches the one we are substituting for. *)
       | Eq  => u

       (* Index was free in the original expression.
          As we've removed the outermost binder, also decrease this
          index by one. *)
       | Gt  => XVar (ix - 1)

       (* Index was bound in the original expression. *)
       | Lt  => XVar ix
       end

    (* Increase the depth as we move across a lambda.
       Also lift free references in the exp being substituted
       across the lambda as we enter it. *)
    |  XLam t1 x2   => XLam t1 (substX (S d) (liftX 0 u) x2)

    |  XApp x1 x2   => XApp (substX d u x1) (substX d u x2)

    (* Fixpoints **********************)
    |  XFix t1 x2   => XFix t1 (substX (S d) (liftX 0 u) x2)

    (* Naturals ***********************)
    |  XNat _       => xx
    |  XSucc x1     => XSucc (substX d u x1)
    |  XPred x1     => XPred (substX d u x1)

    (* Booleans **********************)
    |  XTrue        => xx
    |  XFalse       => xx
    |  XIsZero x1   => XIsZero (substX d u x1)

    (* Branching *********************)
    |  XIf x1 x2 x3
    => XIf (substX d u x1) (substX d u x2) (substX d u x3)
 end.

author: discus-lang

repo: iron

save_path: github-repos/coq/discus-lang-iron


text:
chapter \<open>V-Sets, Epsilon Closure, Ranks\<close>

theory Rank imports Ordinal
begin

section \<open>V-sets\<close>

text \<open>Definition 4.1\<close>
definition Vset :: "hf \<Rightarrow> hf"
  where "Vset x = ord_rec 0 HPow (\<lambda>z. 0) x"

lemma Vset_0 [simp]: "Vset 0 = 0"
  by (simp add: Vset_def)

lemma Vset_succ [simp]: "Ord k \<Longrightarrow> Vset (succ k) = HPow (Vset k)"
  by (simp add: Vset_def)

lemma Vset_non [simp]: "\<not> Ord x \<Longrightarrow> Vset x = 0"
  by (simp add: Vset_def)

text \<open>Theorem 4.2(a)\<close>
lemma Vset_mono_strict:
  assumes "Ord m" "n \<^bold>\<in> m" shows "Vset n < Vset m"
proof -
  have n: "Ord n"
    by (metis Ord_in_Ord assms)
  hence "Ord m \<Longrightarrow> n \<^bold>\<in> m \<Longrightarrow> Vset n < Vset m"
  proof (induct n arbitrary: m rule: Ord_induct2)
    case 0 thus ?case
      by (metis HPow_iff Ord_cases Vset_0 Vset_succ hemptyE le_imp_less_or_eq zero_le)
  next
    case (succ n)
    then show ?case using \<open>Ord m\<close>
      by (metis Ord_cases hemptyE HPow_mono_strict_iff Vset_succ mem_succ_iff)
  qed
  thus ?thesis using assms .
qed

lemma Vset_mono: "\<lbrakk>Ord m; n \<le> m\<rbrakk> \<Longrightarrow> Vset n \<le> Vset m"
  by (metis Ord_linear2 Vset_mono_strict Vset_non order.order_iff_strict
            order_class.order.antisym zero_le)

text \<open>Theorem 4.2(b)\<close>
lemma Vset_Transset: "Ord m \<Longrightarrow> Transset (Vset m)"
  by (induct rule: Ord_induct2) (auto simp: Transset_def)

lemma Ord_sup [simp]: "Ord k \<Longrightarrow> Ord l \<Longrightarrow> Ord (k \<squnion> l)"
  by (metis Ord_linear_le le_iff_sup sup_absorb1)

lemma Ord_inf [simp]: "Ord k \<Longrightarrow> Ord l \<Longrightarrow> Ord (k \<sqinter> l)"
  by (metis Ord_linear_le inf_absorb2 le_iff_inf)

text \<open>Theorem 4.3\<close>
lemma Vset_universal: "\<exists>n. Ord n \<and> x \<^bold>\<in> Vset n"
proof (induct x rule: hf_induct)
  case 0 thus ?case
    by (metis HPow_iff Ord_0 Ord_succ Vset_succ zero_le)
next
  case (hinsert a b)
  then obtain na nb where nab: "Ord na" "a \<^bold>\<in> Vset na" "Ord nb" "b \<^bold>\<in> Vset nb"
    by blast
  hence "b \<le> Vset nb" using Vset_Transset [of nb]
    by (auto simp: Transset_def)
  also have "... \<le> Vset (na \<squnion> nb)" using nab
    by (metis Ord_sup Vset_mono sup_ge2)
  finally have "b \<triangleleft> a \<^bold>\<in> Vset (succ (na \<squnion> nb))" using nab
    by simp (metis Ord_sup Vset_mono sup_ge1 rev_hsubsetD)
  thus ?case using nab
    by (metis Ord_succ Ord_sup)
qed

section \<open>Least Ordinal Operator\<close>

text \<open>Definition 4.4. For every x, let rank(x) be the least ordinal n such that...\<close>

lemma Ord_minimal:
   "Ord k \<Longrightarrow> P k \<Longrightarrow> \<exists>n. Ord n \<and> P n \<and> (\<forall>m. Ord m \<and> P m \<longrightarrow> n \<le> m)"
  by (induct k rule: Ord_induct) (metis Ord_linear2)

lemma OrdLeastI: "Ord k \<Longrightarrow> P k \<Longrightarrow> P(LEAST n. Ord n \<and> P n)"
by (metis (lifting, no_types) Least_equality Ord_minimal)

lemma OrdLeast_le: "Ord k \<Longrightarrow> P k \<Longrightarrow> (LEAST n. Ord n \<and> P n) \<le> k"
by (metis (lifting, no_types) Least_equality Ord_minimal)

lemma OrdLeast_Ord:
  assumes "Ord k" "P k"shows "Ord(LEAST n. Ord n \<and> P n)"
proof -
  obtain n where "Ord n" "P n" "\<forall>m. Ord m \<and> P m \<longrightarrow> n \<le> m"
    by (metis Ord_minimal assms)
  thus ?thesis
    by (metis (lifting) Least_equality)
qed

section \<open>Rank Function\<close>

definition rank :: "hf \<Rightarrow> hf"
  where "rank x = (LEAST n. Ord n \<and> x \<^bold>\<in> Vset (succ n))"

lemma in_Vset_rank: "a \<^bold>\<in> Vset(succ(rank a))"
proof -
  from Vset_universal [of a]
  obtain na where na: "Ord na" "a \<^bold>\<in> Vset (succ na)"
    by (metis Ord_Union Ord_in_Ord Ord_pred Vset_0 hempty_iff)
  thus ?thesis
    by (unfold rank_def) (rule OrdLeastI)
qed

lemma Ord_rank [simp]: "Ord (rank a)"
  by (metis Ord_succ_iff Vset_non hemptyE in_Vset_rank)

lemma le_Vset_rank: "a \<le> Vset(rank a)"
  by (metis HPow_iff Ord_succ_iff Vset_non Vset_succ hemptyE in_Vset_rank)

lemma VsetI: "succ(rank a) \<le> k \<Longrightarrow> Ord k \<Longrightarrow> a \<^bold>\<in> Vset k"
  by (metis Vset_mono hsubsetCE in_Vset_rank)

lemma Vset_succ_rank_le: "Ord k \<Longrightarrow> a \<^bold>\<in> Vset (succ k) \<Longrightarrow> rank a \<le> k"
  by (unfold rank_def) (rule OrdLeast_le)

lemma Vset_rank_lt: assumes a: "a \<^bold>\<in> Vset k" shows "rank a < k"
proof -
  { assume k: "Ord k"
    hence ?thesis
    proof (cases k rule: Ord_cases)
      case 0 thus ?thesis using a
        by simp
    next
      case (succ l) thus ?thesis using a
        by (metis Ord_lt_succ_iff_le Ord_succ_iff Vset_non Vset_succ_rank_le hemptyE in_Vset_rank)
    qed
  }
  thus ?thesis using a
    by (metis Vset_non hemptyE)
qed

text \<open>Theorem 4.5\<close>
theorem rank_lt: "a \<^bold>\<in> b \<Longrightarrow> rank(a) < rank(b)"
  by (metis Vset_rank_lt hsubsetD le_Vset_rank)

lemma rank_mono: "x \<le> y \<Longrightarrow> rank x \<le> rank y"
  by (metis HPow_iff Ord_rank Vset_succ Vset_succ_rank_le dual_order.trans le_Vset_rank)

lemma rank_sup [simp]: "rank (a \<squnion> b) = rank a \<squnion> rank b"
proof (rule antisym)
  have o: "Ord (rank a \<squnion> rank b)"
    by simp
  thus "rank (a \<squnion> b) \<le> rank a \<squnion> rank b"
    apply (rule Vset_succ_rank_le, simp)
    apply (metis le_Vset_rank order_trans Vset_mono sup_ge1 sup_ge2 o)
    done
next
  show "rank a \<squnion> rank b \<le> rank (a \<squnion> b)"
    by (metis le_supI le_supI1 le_supI2 order_eq_refl rank_mono)
qed

lemma rank_singleton [simp]: "rank \<lbrace>a\<rbrace> = succ(rank a)"
proof -
  have oba: "Ord (succ (rank a))"
    by simp
  show ?thesis
    proof (rule antisym)
      show "rank \<lbrace>a\<rbrace> \<le> succ (rank a)"
        by (metis Vset_succ_rank_le HPow_iff Vset_succ in_Vset_rank less_eq_insert1_iff oba zero_le)
    next
      show "succ (rank a) \<le> rank\<lbrace>a\<rbrace>"
        by (metis Ord_linear_le Ord_lt_succ_iff_le rank_lt Ord_rank hmem_hinsert less_le_not_le oba)
    qed
qed

lemma rank_hinsert [simp]: "rank (b \<triangleleft> a) = rank b \<squnion> succ(rank a)"
  by (metis hinsert_eq_sup rank_singleton rank_sup)

text \<open>Definition 4.6. The transitive closure of @{term x} is
 the minimal transitive set @{term y} such that @{term"x\<le>y"}.\<close>

section \<open>Epsilon Closure\<close>

definition
  eclose    :: "hf \<Rightarrow> hf"  where
    "eclose X = \<Sqinter> \<lbrace>Y \<^bold>\<in> HPow(Vset (rank X)). Transset Y \<and> X\<le>Y\<rbrace>"

lemma eclose_facts:
  shows Transset_eclose: "Transset (eclose X)"
   and  le_eclose: "X \<le> eclose X"
proof -
  have nz: "\<lbrace>Y \<^bold>\<in> HPow(Vset (rank X)). Transset Y \<and> X\<le>Y\<rbrace> \<noteq> 0"
    by (simp add: eclose_def hempty_iff) (metis Ord_rank Vset_Transset le_Vset_rank order_refl)
  show "Transset (eclose X)" "X \<le> eclose X" using HInter_iff [OF nz]
    by (auto simp: eclose_def Transset_def)
qed

lemma eclose_minimal:
  assumes Y: "Transset Y" "X\<le>Y" shows "eclose X \<le> Y"
proof -
  have "\<lbrace>Y \<^bold>\<in> HPow(Vset (rank X)). Transset Y \<and> X\<le>Y\<rbrace> \<noteq> 0"
    by (simp add: eclose_def hempty_iff) (metis Ord_rank Vset_Transset le_Vset_rank order_refl)
  moreover have "Transset (Y \<sqinter> Vset (rank X))"
    by (metis Ord_rank Transset_inf Vset_Transset Y(1))
  moreover have "X \<le> Y \<sqinter> Vset (rank X)"
    by (metis Y(2) le_Vset_rank le_inf_iff)
  ultimately show "eclose X \<le> Y"
    apply (auto simp: eclose_def)
    apply (metis hinter_iff le_inf_iff order_refl)
    done
qed

lemma eclose_0 [simp]: "eclose 0 = 0"
  by (metis Ord_0 Vset_0 Vset_Transset eclose_minimal less_eq_hempty)

lemma eclose_sup [simp]: "eclose (a \<squnion> b) = eclose a \<squnion> eclose b"
proof (rule order_antisym)
  show "eclose (a \<squnion> b) \<le> eclose a \<squnion> eclose b"
    by (metis Transset_eclose Transset_sup eclose_minimal le_eclose sup_mono)
next
  show "eclose a \<squnion> eclose b \<le> eclose (a \<squnion> b)"
    by (metis Transset_eclose eclose_minimal le_eclose le_sup_iff)
qed

lemma eclose_singleton [simp]: "eclose \<lbrace>a\<rbrace> = (eclose a) \<triangleleft> a"
proof (rule order_antisym)
  show "eclose \<lbrace>a\<rbrace> \<le> eclose a \<triangleleft> a"
    by (metis eclose_minimal Transset_eclose Transset_hinsert
              le_eclose less_eq_insert1_iff order_refl zero_le)
next
  show "eclose a \<triangleleft> a \<le> eclose \<lbrace>a\<rbrace>"
    by (metis Transset_def Transset_eclose eclose_minimal le_eclose less_eq_insert1_iff)
qed

lemma eclose_hinsert [simp]: "eclose (b \<triangleleft> a) = eclose b \<squnion> (eclose a \<triangleleft> a)"
  by (metis eclose_singleton eclose_sup hinsert_eq_sup)

lemma eclose_succ [simp]: "eclose (succ a) = eclose a \<triangleleft> a"
  by (auto simp: succ_def)

lemma fst_in_eclose [simp]: "x \<^bold>\<in> eclose \<langle>x, y\<rangle>"
  by (metis eclose_hinsert hmem_hinsert hpair_def hunion_iff)

lemma snd_in_eclose [simp]: "y \<^bold>\<in> eclose \<langle>x, y\<rangle>"
  by (metis eclose_hinsert hmem_hinsert hpair_def hunion_iff)

text \<open>Theorem 4.7. rank(x) = rank(cl(x)).\<close>
lemma rank_eclose [simp]: "rank (eclose x) = rank x"
proof (induct x rule: hf_induct)
  case 0 thus ?case by simp
next
  case (hinsert a b) thus ?case
    by simp (metis hinsert_eq_sup succ_def sup.left_idem)
qed

section \<open>Epsilon-Recursion\<close>

text \<open>Theorem 4.9.  Definition of a function by recursion on rank.\<close>

lemma hmem_induct [case_names step]:
  assumes ih: "\<And>x. (\<And>y. y \<^bold>\<in> x \<Longrightarrow> P y) \<Longrightarrow> P x" shows "P x"
proof -
  have "\<And>y. y \<^bold>\<in> x \<Longrightarrow> P y"
  proof (induct x rule: hf_induct)
    case 0 thus ?case by simp
  next
    case (hinsert a b) thus ?case
      by (metis assms hmem_hinsert)
  qed
  thus ?thesis by (metis ih)
qed

definition
  hmem_rel :: "(hf * hf) set" where
  "hmem_rel = trancl {(x,y). x \<^bold>\<in> y}"

lemma wf_hmem_rel: "wf hmem_rel"
proof -
  have "wf {(x,y). x \<^bold>\<in> y}"
    by (metis (full_types) hmem_induct wfPUNIVI wfP_def)
  thus ?thesis
    by (metis hmem_rel_def wf_trancl)
qed

lemma hmem_eclose_le: "y \<^bold>\<in> x \<Longrightarrow> eclose y \<le> eclose x"
  by (metis Transset_def Transset_eclose eclose_minimal hsubsetD le_eclose)

lemma hmem_rel_iff_hmem_eclose: "(x,y) \<in> hmem_rel \<longleftrightarrow> x \<^bold>\<in> eclose y"
proof (unfold hmem_rel_def, rule iffI)
  assume "(x, y) \<in> trancl {(x, y). x \<^bold>\<in> y}"
  thus "x \<^bold>\<in> eclose y"
    proof (induct rule: trancl_induct)
      case (base y) thus ?case
        by (metis hsubsetCE le_eclose mem_Collect_eq split_conv)
    next
      case (step y z) thus ?case
        by (metis hmem_eclose_le hsubsetD mem_Collect_eq split_conv)
    qed
next
  have "Transset \<lbrace>x \<^bold>\<in> eclose y. (x, y) \<in> hmem_rel\<rbrace>" using Transset_eclose
    by (auto simp: Transset_def hmem_rel_def intro: trancl_trans)
  hence "eclose y \<le> \<lbrace>x \<^bold>\<in> eclose y. (x, y) \<in> hmem_rel\<rbrace>"
    by (rule eclose_minimal) (auto simp: le_HCollect_iff le_eclose hmem_rel_def)
  moreover assume "x \<^bold>\<in> eclose y"
  ultimately show "(x, y) \<in> trancl {(x, y). x \<^bold>\<in> y}"
    by (metis HCollect_iff hmem_rel_def hsubsetD)
qed

definition hmemrec :: "((hf \<Rightarrow> 'a) \<Rightarrow> hf \<Rightarrow> 'a) \<Rightarrow> hf \<Rightarrow> 'a" where
  "hmemrec G \<equiv> wfrec hmem_rel G"

definition ecut :: "(hf \<Rightarrow> 'a) \<Rightarrow> hf \<Rightarrow> hf \<Rightarrow> 'a" where
  "ecut f x \<equiv> (\<lambda>y. if y \<^bold>\<in> eclose x then f y else undefined)"

lemma hmemrec: "hmemrec G a = G (ecut (hmemrec G) a) a"
  by (simp add: cut_def ecut_def hmem_rel_iff_hmem_eclose def_wfrec [OF hmemrec_def wf_hmem_rel])

text \<open>This form avoids giant explosions in proofs.\<close>
lemma def_hmemrec: "f \<equiv> hmemrec G \<Longrightarrow> f a = G (ecut (hmemrec G) a) a"
  by (metis hmemrec)

lemma ecut_apply: "y \<^bold>\<in> eclose x \<Longrightarrow> ecut f x y = f y"
  by (metis ecut_def)

lemma RepFun_ecut: "y \<le> z \<Longrightarrow> RepFun y (ecut f z) = RepFun y f"
  apply (auto simp: hf_ext)
  apply (metis ecut_def hsubsetD le_eclose)
  apply (metis ecut_apply le_eclose hsubsetD)
  done

text \<open>Now, a stronger induction rule, for the transitive closure of membership\<close>
lemma hmem_rel_induct [case_names step]:
  assumes ih: "\<And>x. (\<And>y. (y,x) \<in> hmem_rel \<Longrightarrow> P y) \<Longrightarrow> P x" shows "P x"
proof -
  have "\<And>y. (y,x) \<in> hmem_rel \<Longrightarrow> P y"
  proof (induct x rule: hf_induct)
    case 0 thus ?case
      by (metis eclose_0 hmem_hempty hmem_rel_iff_hmem_eclose)
  next
    case (hinsert a b)
    thus ?case
      by (metis assms eclose_hinsert hmem_hinsert hmem_rel_iff_hmem_eclose hunion_iff)
  qed
  thus ?thesis  by (metis assms)
qed

lemma rank_HUnion_less:  "x \<noteq> 0 \<Longrightarrow> rank (\<Squnion>x) < rank x"
  apply (induct x rule: hf_induct, auto)
  apply (metis hmem_hinsert rank_hinsert rank_lt)
  apply (metis HUnion_hempty Ord_lt_succ_iff_le Ord_rank hunion_hempty_right
               less_supI1 less_supI2 rank_sup sup.cobounded2)
  done

corollary Sup_ne: "x \<noteq> 0 \<Longrightarrow> \<Squnion>x \<noteq> x"
  by (metis less_irrefl rank_HUnion_less)

end

repo: PSL


text:
theory T117
imports Main
begin
lemma "(
(\<forall> x::nat. \<forall> y::nat. meet(x, y) = meet(y, x)) &
(\<forall> x::nat. \<forall> y::nat. join(x, y) = join(y, x)) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(x, meet(y, z)) = meet(meet(x, y), z)) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(x, join(y, z)) = join(join(x, y), z)) &
(\<forall> x::nat. \<forall> y::nat. meet(x, join(x, y)) = x) &
(\<forall> x::nat. \<forall> y::nat. join(x, meet(x, y)) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(x, join(y, z)) = join(mult(x, y), mult(x, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(join(x, y), z) = join(mult(x, z), mult(y, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(x, over(join(mult(x, y), z), y)) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(y, undr(x, join(mult(x, y), z))) = y) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(mult(over(x, y), y), x) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(mult(y, undr(y, x)), x) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. undr(x, join(y, z)) = join(undr(x, y), undr(x, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. over(x, meet(y, z)) = join(over(x, y), over(x, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. undr(meet(x, y), z) = join(undr(x, z), undr(y, z))) &
(\<forall> x::nat. \<forall> y::nat. invo(join(x, y)) = meet(invo(x), invo(y))) &
(\<forall> x::nat. \<forall> y::nat. invo(meet(x, y)) = join(invo(x), invo(y))) &
(\<forall> x::nat. invo(invo(x)) = x)
) \<longrightarrow>
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. over(join(x, y), z) = join(over(x, z), over(y, z)))
"
nitpick[card nat=8,timeout=86400]
oops
end

author: inpefess

repo: residuated-binars


text:
(*  Title:      HOL/MicroJava/BV/JVM.thy
    Author:     Tobias Nipkow, Gerwin Klein
    Copyright   2000 TUM
*)

section \<open>Kildall for the JVM \label{sec:JVM}\<close>

theory BVExec
imports
  "../DFA/Abstract_BV"
  TF_JVM
begin

definition kiljvm :: "'addr jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow>
                    'addr instr list \<Rightarrow> ex_table \<Rightarrow> ty\<^sub>i' err list \<Rightarrow> ty\<^sub>i' err list"
where
  "kiljvm P mxs mxl T\<^sub>r is xt \<equiv>
  kildall (JVM_SemiType.le P mxs mxl) (JVM_SemiType.sup P mxs mxl)
          (exec P mxs T\<^sub>r xt is)"

definition  wt_kildall :: "'addr jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
                         'addr instr list \<Rightarrow> ex_table \<Rightarrow> bool"
where
  "wt_kildall P C' Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<equiv>
   0 < size is \<and>
   (let first  = Some ([],[OK (Class C')]@(map OK Ts)@(replicate mxl\<^sub>0 Err));
        start  = OK first#(replicate (size is - 1) (OK None));
        result = kiljvm P mxs (1+size Ts+mxl\<^sub>0) T\<^sub>r is xt  start
    in \<forall>n < size is. result!n \<noteq> Err)"

definition wf_jvm_prog\<^sub>k :: "'addr jvm_prog \<Rightarrow> bool"
where
  "wf_jvm_prog\<^sub>k P \<equiv>
  wf_prog (\<lambda>P C' (M,Ts,T\<^sub>r,(mxs,mxl\<^sub>0,is,xt)). wt_kildall P C' Ts T\<^sub>r mxs mxl\<^sub>0 is xt) P"

theorem (in start_context) is_bcv_kiljvm:
  "is_bcv r Err step (size is) A (kiljvm P mxs mxl T\<^sub>r is xt)"
(*<*)
  apply (insert wf)
  apply (unfold kiljvm_def)
  apply (fold r_def f_def step_def_exec)
  apply (rule is_bcv_kildall)
       apply simp
       apply (rule Semilat.intro)
       apply (fold sl_def2, erule semilat_JVM)
      apply simp
      apply blast
     apply (simp add: JVM_le_unfold)
    apply (rule exec_pres_type)
   apply (rule bounded_step)
  apply (erule step_mono)
  done
(*>*)

(* FIXME: move? *)
lemma subset_replicate [intro?]: "set (replicate n x) \<subseteq> {x}"
  by (induct n) auto

lemma in_set_replicate:
  assumes "x \<in> set (replicate n y)"
  shows "x = y"
(*<*)
proof -
  note assms
  also have "set (replicate n y) \<subseteq> {y}" ..
  finally show ?thesis by simp
qed
(*>*)

lemma (in start_context) start_in_A [intro?]:
  "0 < size is \<Longrightarrow> start \<in> list (size is) A"
  using Ts C
(*<*)
  apply (simp add: JVM_states_unfold)
  apply (force intro!: listI list_appendI dest!: in_set_replicate)
  done
(*>*)

theorem (in start_context) wt_kil_correct:
  assumes wtk: "wt_kildall P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt"
  shows "\<exists>\<tau>s. wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
(*<*)
proof -
  from wtk obtain res where
    result:   "res = kiljvm P mxs mxl T\<^sub>r is xt start" and
    success:  "\<forall>n < size is. res!n \<noteq> Err" and
    instrs:   "0 < size is"
    by (unfold wt_kildall_def) simp

  have bcv: "is_bcv r Err step (size is) A (kiljvm P mxs mxl T\<^sub>r is xt)"
    by (rule is_bcv_kiljvm)

  from instrs have "start \<in> list (size is) A" ..
  with bcv success result have
    "\<exists>ts\<in>list (size is) A. start [\<sqsubseteq>\<^sub>r] ts \<and> wt_step r Err step ts"
    by (unfold is_bcv_def) blast
  then obtain \<tau>s' where
    in_A: "\<tau>s' \<in> list (size is) A" and
    s:    "start [\<sqsubseteq>\<^sub>r] \<tau>s'" and
    w:    "wt_step r Err step \<tau>s'"
    by blast
  hence wt_err_step: "wt_err_step (sup_state_opt P) step \<tau>s'"
    by (simp add: wt_err_step_def JVM_le_Err_conv)

  from in_A have l: "size \<tau>s' = size is" by simp
  moreover {
    from in_A  have "check_types P mxs mxl \<tau>s'" by (simp add: check_types_def)
    also from w have "\<forall>x \<in> set \<tau>s'. x \<noteq> Err"
      by (auto simp add: wt_step_def all_set_conv_all_nth)
    hence [symmetric]: "map OK (map ok_val \<tau>s') = \<tau>s'"
      by (auto intro!: map_idI simp add: wt_step_def)
    finally  have "check_types P mxs mxl (map OK (map ok_val \<tau>s'))" .
  }
  moreover {
    from s have "start!0 \<sqsubseteq>\<^sub>r \<tau>s'!0" by (rule le_listD) simp
    moreover
    from instrs w l
    have "\<tau>s'!0 \<noteq> Err" by (unfold wt_step_def) simp
    then obtain \<tau>s0 where "\<tau>s'!0 = OK \<tau>s0" by auto
    ultimately
    have "wt_start P C Ts mxl\<^sub>0 (map ok_val \<tau>s')" using l instrs
      by (unfold wt_start_def)
         (simp add: lesub_def JVM_le_Err_conv Err.le_def)
  }
  moreover
  from in_A have "set \<tau>s' \<subseteq> A" by simp
  with wt_err_step bounded_step
  have "wt_app_eff (sup_state_opt P) app eff (map ok_val \<tau>s')"
    by (auto intro: wt_err_imp_wt_app_eff simp add: l)
  ultimately
  have "wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt (map ok_val \<tau>s')"
    using instrs by (simp add: wt_method_def2 check_types_def del: map_map)
  thus ?thesis by blast
qed
(*>*)

theorem (in start_context) wt_kil_complete:
  assumes wtm: "wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"
  shows "wt_kildall P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt"
(*<*)
proof -
  from wtm obtain
    instrs:   "0 < size is" and
    length:   "length \<tau>s = length is" and
    ck_type:  "check_types P mxs mxl (map OK \<tau>s)" and
    wt_start: "wt_start P C Ts mxl\<^sub>0 \<tau>s" and
    app_eff:  "wt_app_eff (sup_state_opt P) app eff \<tau>s"
    by (simp add: wt_method_def2 check_types_def)

  from ck_type
  have in_A: "set (map OK \<tau>s) \<subseteq> A"
    by (simp add: check_types_def)
  with app_eff in_A bounded_step
  have "wt_err_step (sup_state_opt P) (err_step (size \<tau>s) app eff) (map OK \<tau>s)"
    by - (erule wt_app_eff_imp_wt_err,
          auto simp add: exec_def length states_def)
  hence wt_err: "wt_err_step (sup_state_opt P) step (map OK \<tau>s)"
    by (simp add: length)
  have is_bcv: "is_bcv r Err step (size is) A (kiljvm P mxs mxl T\<^sub>r is xt)"
    by (rule is_bcv_kiljvm)
  moreover from instrs have "start \<in> list (size is) A" ..
  moreover
  let ?\<tau>s = "map OK \<tau>s"
  have less_\<tau>s: "start [\<sqsubseteq>\<^sub>r] ?\<tau>s"
  proof (rule le_listI)
    from length instrs
    show "length start = length (map OK \<tau>s)" by simp
  next
    fix n
    from wt_start have "P \<turnstile> ok_val (start!0) \<le>' \<tau>s!0"
      by (simp add: wt_start_def)
    moreover from instrs length have "0 < length \<tau>s" by simp
    ultimately have "start!0 \<sqsubseteq>\<^sub>r ?\<tau>s!0"
      by (simp add: JVM_le_Err_conv lesub_def)
    moreover {
      fix n'
      have "OK None \<sqsubseteq>\<^sub>r ?\<tau>s!n"
        by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def
                 split: err.splits)
      hence "\<lbrakk>n = Suc n'; n < size start\<rbrakk> \<Longrightarrow> start!n \<sqsubseteq>\<^sub>r ?\<tau>s!n" by simp
    }
    ultimately
    show "n < size start \<Longrightarrow> start!n \<sqsubseteq>\<^sub>r ?\<tau>s!n" by (cases n, blast+)
  qed
  moreover
  from ck_type length
  have "?\<tau>s \<in> list (size is) A"
    by (auto intro!: listI simp add: check_types_def)
  moreover
  from wt_err have "wt_step r Err step ?\<tau>s"
    by (simp add: wt_err_step_def JVM_le_Err_conv)
  ultimately
  have "\<forall>p. p < size is \<longrightarrow> kiljvm P  mxs mxl T\<^sub>r is xt start ! p \<noteq> Err"
    by (unfold is_bcv_def) blast
  with instrs
  show "wt_kildall P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt" by (unfold wt_kildall_def) simp
qed
(*>*)

theorem jvm_kildall_correct:
  "wf_jvm_prog\<^sub>k P = wf_jvm_prog P"
(*<*)
proof
  let ?\<Phi> = "\<lambda>C M. let (C,Ts,T\<^sub>r,meth) = method P C M; (mxs,mxl\<^sub>0,is,xt) = the meth in
              SOME \<tau>s. wt_method P C Ts T\<^sub>r mxs mxl\<^sub>0 is xt \<tau>s"

  \<comment> \<open>soundness\<close>
  assume wt: "wf_jvm_prog\<^sub>k P"
  hence "wf_jvm_prog\<^bsub>?\<Phi>\<^esub> P"
    apply (unfold wf_jvm_prog_phi_def wf_jvm_prog\<^sub>k_def)
    apply (erule wf_prog_lift)
    apply (auto intro: someI_ex[OF start_context.wt_kil_correct [OF start_context.intro]])
    done
  thus "wf_jvm_prog P" by (unfold wf_jvm_prog_def) fast
next
  \<comment> \<open>completeness\<close>
  assume wt: "wf_jvm_prog P"
  thus "wf_jvm_prog\<^sub>k P"
    apply (unfold wf_jvm_prog_def wf_jvm_prog_phi_def wf_jvm_prog\<^sub>k_def)
    apply (clarify)
    apply (erule wf_prog_lift)
    apply (auto intro!: start_context.wt_kil_complete start_context.intro)
    done
qed
(*>*)

end


text:
theory ArityAnalysisSig
imports "../Launchbury/Terms" AEnv "Arity-Nominal" "../Launchbury/Nominal-HOLCF"  "../Launchbury/Substitution"
begin

locale ArityAnalysis =
  fixes Aexp :: "exp \<Rightarrow> Arity \<rightarrow> AEnv"
begin
  abbreviation Aexp_syn ("\<A>\<^bsub>_\<^esub>")where "\<A>\<^bsub>a\<^esub> e \<equiv> Aexp e\<cdot>a"
  abbreviation Aexp_bot_syn ("\<A>\<^sup>\<bottom>\<^bsub>_\<^esub>")
    where "\<A>\<^sup>\<bottom>\<^bsub>a\<^esub> e \<equiv> fup\<cdot>(Aexp e)\<cdot>a"

end

locale ArityAnalysisHeap =
  fixes Aheap :: "heap \<Rightarrow> exp \<Rightarrow> Arity \<rightarrow> AEnv"

locale EdomArityAnalysis = ArityAnalysis +
  assumes Aexp_edom: "edom (\<A>\<^bsub>a\<^esub> e) \<subseteq> fv e"
begin

  lemma fup_Aexp_edom: "edom (\<A>\<^sup>\<bottom>\<^bsub>a\<^esub> e) \<subseteq> fv e"
    by (cases a) (auto dest:set_mp[OF Aexp_edom])

  lemma Aexp_fresh_bot[simp]: assumes "atom v \<sharp> e" shows "\<A>\<^bsub>a\<^esub> e v = \<bottom>"
  proof-
    from assms have "v \<notin> fv e" by (metis fv_not_fresh)
    with Aexp_edom have "v \<notin> edom (\<A>\<^bsub>a\<^esub> e)" by auto
    thus ?thesis unfolding edom_def by simp
  qed
end

locale ArityAnalysisHeapEqvt = ArityAnalysisHeap +
  assumes Aheap_eqvt[eqvt]: "\<pi> \<bullet> Aheap = Aheap"

end

author: nomeata

repo: isa-launchbury