Ignore:
Timestamp:
Feb 22, 2013, 3:27:16 PM (8 years ago)
Author:
sacerdot
Message:
  1. proof closed in ASM/UtilBranch
  2. more passes integrated in the compiler.ma
  3. some work on commenting out broken proofs in linearise.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/linearise.ma

    r2570 r2702  
    256256    cases s in H3; [3: *]
    257257    [ * ] normalize nodelta
    258     [1,3: [#f #args #dest |#s'] #nxt * #EQnth_opt #H %{EQnth_opt}
     258    [2,4: [#f #args #dest |#s'] #nxt * #EQnth_opt #H %{EQnth_opt}
    259259      inversion (lookup … visited nxt) in H; [2: #n'] #EQlookup
    260260      normalize nodelta *
     
    264264        whd in ⊢ (?%→?); >EQlookup *
    265265      ]
    266     | #a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1}
     266    |3: #a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1}
    267267      inversion (lookup … visited lfalse) in H2;
    268268      [ #ABS * #H' lapply (All_nth … H … H')
     
    270270      | #n' #_ normalize nodelta #EQ >EQ %
    271271      ]
    272     | #s #H @H
     272    | #s #H (*CSC XXXXXXXXXXXXXXXXXXXX @H *)
    273273    ]
    274274  ]
     
    327327  #P whd in match add_req_gen;
    328328  cases statement [ * [#f #args #dest|  #a #ltrue | #s ] #nxt | #s | * ]
    329 [2,4: normalize nodelta #H #_ @(H I) ]
    330   normalize nodelta inversion (nxt ∈ visited') #EQ normalize nodelta
    331   #H1 #H2 [1,3: @(H2 … (refl …)) >EQ % |*: @H1 % * ]
     329 [2,4: normalize nodelta #l #H1 #H2 lapply (H2 … (refl …)) -H2
     330      cases (l ∈ add …) in H1; normalize nodelta #H1 #H2 try @H2 try @H1 try %
     331      //
     332 |3,5: normalize nodelta [#_] #H #_ @H %
     333 | normalize nodelta in dest nxt ⊢ %; inversion (args ∈ add …) #EQ
     334   normalize nodelta [ @nxt | @dest ] >EQ try % ]
     335|14: skip
     336] cases daemon (*CSC: XXXXXXXXX
    332337|3: elim H #pre ** #H1 #H2 #_
    333338  #i >mem_set_union
     
    336341    #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption
    337342  | >mem_set_union
    338     #H elim (orb_Prop_true … H) -H
     343    #H elim (orb_Prop_true … H) -H (*CSC XXXXXXXXXX
    339344    [ #i_expl %1 @Exists_append_l
    340345      lapply i_expl whd in match translated_statement;
     
    361366        #i_vis %2 >mem_set_add @orb_Prop_r assumption
    362367      ]
    363     ]
     368    ]*) cases daemon
    364369  ]
    365370|4,5,6: change with reverse in match rev;
     
    418423        lapply (in_map_domain … visited vis_hd)
    419424        >H3 normalize nodelta //
    420       | %{statement}
     425      | %{statement}  (*CSC XXXXXXX
    421426        %
    422427        [ @lookup_eq_safe
     
    438443            |*: %%
    439444            ]
    440           ]
     445          ]*) cases daemon
    441446        ]
    442447      ]
    443448    | #NEQ #n_i >(lookup_add_miss … visited … NEQ)
     449      cases daemon (*CSC XXXX
    444450      #Hlookup elim (generated_prf1 … Hlookup)
    445451      #G1 * #s * #G2 #G3
     
    481487          ]
    482488        ]
    483       ]
     489      ] *)
    484490    ]
    485491  | #i whd in match visited';
     
    509515  @add_req_gen_prf [ #_ | #s #next #_ #_ ] normalize >gen_length_prf %
    510516|
    511 ]
     517]*)
    512518qed.
    513519
     
    644650               (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨
    645651               (stmt_at … c n = Some ? (FCOND … I a ltrue nxt))
     652             | CALL _ _ _ ⇒
     653               (stmt_at … c n = Some ? (sequential … s' it)) ∧
     654                  ((sigma nxt = Some ? (S n)) ∨
     655                   (stmt_at … c (S n) = Some ? (GOTO … nxt)))               
     656             | COST_LABEL _ ⇒
     657               (stmt_at … c n = Some ? (sequential … s' it)) ∧
     658                  ((sigma nxt = Some ? (S n)) ∨
     659                   (stmt_at … c (S n) = Some ? (GOTO … nxt)))               
    646660             ]
    647661           | final s' ⇒
     
    829843  〈«mk_joint_internal_function (mk_lin_params p) globals
    830844   (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig)
    831    (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) (joint_if_locals ?? f_sig)
    832    (joint_if_stacksize ?? f_sig) code entry entry (* exit is dummy! *), ?»,
     845   (joint_if_result ?? f_sig) (joint_if_params ?? f_sig)
     846   (joint_if_stacksize ?? f_sig) code entry, ?»,
    833847   sigma〉.
    834848normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.