Changeset 3145 for src/joint


Ignore:
Timestamp:
Apr 15, 2013, 4:31:50 PM (7 years ago)
Author:
tranquil
Message:
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
Location:
src/joint
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r3037 r3145  
    630630definition stack_cost_model ≝ list (ident × nat).
    631631
     632(* move! *)
     633let rec list_map_opt A B (f : A → option B) (l : list A) on l : list B ≝
     634match l with
     635[ nil ⇒ [ ]
     636| cons hd tl ⇒
     637  (match f hd with [ Some x ⇒ [ x ] | None ⇒ [ ]]) @ list_map_opt … f tl
     638].
     639
    632640definition stack_cost : ∀p:params. joint_program p → stack_cost_model ≝
    633641 λp,pr.
    634   foldr …
    635    (λid_fun,acc. let 〈id,fun〉 ≝ id_fun in
    636      match fun with
    637      [ Internal jif ⇒ 〈id,joint_if_stacksize ?? (pi1 … jif)〉::acc
    638      | External _ ⇒ acc ])
    639    [ ] (prog_funct ?? pr).
     642  list_map_opt …
     643    (λid_fun.match \snd id_fun with
     644      [ Internal jif ⇒ Some ? 〈\fst id_fun, joint_if_stacksize ?? (pi1 … jif)〉
     645      | _ ⇒ None ?
     646      ]) (prog_funct ?? pr).
     647
     648definition stack_sizes : stack_cost_model → ident → option ℕ ≝
     649λm,id.find …
     650  (λpr.if eq_identifier … id (\fst pr) then Some ? (\snd pr) else None ?) m.
    640651
    641652include "common/Globalenvs.ma". (* for size_init_data_list, probably to be moved to AST.ma *)
  • src/joint/Traces.ma

    r3041 r3145  
    4545    (* regs ≝ *)(empty_regsT … spp)
    4646    (* mem ≝ *)m
    47     (* stack_usage ≝ *)globals_size in
     47    (* stack_usage ≝ *)0 in
    4848  return
    4949  mk_state_pc ?
Note: See TracChangeset for help on using the changeset viewer.