Changeset 2774 for src/joint


Ignore:
Timestamp:
Mar 5, 2013, 6:15:06 PM (7 years ago)
Author:
sacerdot
Message:
  1. the compiler now outputs both the stack cost model and the max stack available
  2. hypothesis on initial status not failing removed from correctness.ma by using the low level definition
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2712 r2774  
    530530definition joint_program ≝
    531531 λp:params. program (joint_function p) nat.
     532
     533(* The cost model for stack consumption *)
     534definition stack_cost_model ≝ list (ident × nat).
     535
     536definition stack_cost : ∀p:params. joint_program p → stack_cost_model ≝
     537 λp,pr.
     538  foldr …
     539   (λid_fun,acc. let 〈id,fun〉 ≝ id_fun in
     540     match fun with
     541     [ Internal jif ⇒ 〈id,joint_if_stacksize ?? (pi1 … jif)〉::acc
     542     | External _ ⇒ acc ])
     543   [ ] (prog_funct ?? pr).
     544
Note: See TracChangeset for help on using the changeset viewer.