Ignore:
Timestamp:
Feb 22, 2013, 7:11:30 PM (8 years ago)
Author:
tranquil
Message:

fixed linearise and LINToASM
LINToASM has now correct transformation of idents and labels to Identifier

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semanticsUtils.ma

    r2688 r2708  
    311311* #vars1 #functs1 #main1
    312312* #vars2 #functs2 #main2
    313 * #Mvars #Mfns #EQmain destruct
     313*
     314whd in match prog_var_names;
     315normalize nodelta;
     316#Mvars #Mfns #EQmain destruct
    314317lapply (sym_eq ????)
    315 whd in match prog_var_names in functs2 Mfns ⊢ %;
    316 normalize nodelta in functs2 Mfns ⊢ %; #E
    317 lapply Mfns lapply functs2 -functs2 lapply Mvars -Mvars lapply init_eq -init_eq
     318#E
     319lapply Mfns lapply functs2 -functs2
    318320whd in match globalenv; whd in match globalenv_allocmem;
    319 normalize nodelta
    320 cases daemon
    321 (* TODO I hate coercions *)
     321whd in match prog_var_names in E ⊢ %;
     322normalize nodelta in E ⊢ %;
     323>E normalize nodelta #functs2 #Mfns
     324@add_globals_match [ assumption | % ]
     325@add_functs_match [ assumption ]
     326% try % #p %
    322327qed.
    323328
Note: See TracChangeset for help on using the changeset viewer.