- Timestamp:
- Apr 18, 2011, 12:33:35 PM (10 years ago)
- Location:
- src
- Files:
-
- 5 added
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/cminorMatitaPrinter.ml
r751 r758 16 16 let print_data = function 17 17 | Data_reserve n -> Printf.sprintf "Init_space %d" n 18 | Data_int8 i -> Printf.sprintf "Init_int8 %d" i19 | Data_int16 i -> Printf.sprintf "Init_int16 %d" i20 | Data_int32 i -> Printf.sprintf "Init_int32 %d" i18 | Data_int8 i -> Printf.sprintf "Init_int8 (repr %d)" i 19 | Data_int16 i -> Printf.sprintf "Init_int16 (repr %d)" i 20 | Data_int32 i -> Printf.sprintf "Init_int32 (repr %d)" i 21 21 | Data_float32 f -> Printf.sprintf "Init_float32 %f" f 22 22 | Data_float64 f -> Printf.sprintf "Init_float64 %f" f 23 23 24 24 let print_var n (id, init) = 25 Printf.sprintf "(pair ?? (pair ?? (pair ?? %s [%s]) Any) it)"25 Printf.sprintf "(pair ?? (pair ?? (pair ?? id_%s [%s]) Any) it)" 26 26 id 27 27 (MiscPottier.string_of_list ";" print_data init) … … 298 298 (match main with Some f -> "id_" ^ f | None -> "ident_of_nat 0 (* None! *)") 299 299 300 let define_var_id (id,_) = 301 Printf.sprintf "definition id_%s := ident_of_nat %d.\n" id (fresh ()) 302 303 let define_var_ids = 304 List.fold_left (fun s v -> s ^ (define_var_id v)) "" 305 300 306 let print_program p = 301 Printf.sprintf "include \"Cminor/semantics.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\ndefinition myprog : Cminor_program :=\nmk_program ?? [\n%s\n]%s\n[%s]\n.\n" 307 Printf.sprintf "include \"Cminor/semantics.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\n%s\n\ndefinition myprog : Cminor_program :=\nmk_program ?? [\n%s\n]%s\n[%s]\n.\n" 308 (define_var_ids p.Cminor.vars) 302 309 (print_functs p.Cminor.functs) 303 310 (print_fun' 2 p.Cminor.functs) -
src/common/Globalenvs.ma
r747 r758 447 447 ]. 448 448 449 definition size_init_data_list : list init_data → Z≝450 λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) O Zi_data.449 definition size_init_data_list : list init_data → nat ≝ 450 λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) O i_data. 451 451 452 452 (* Nonessential properties that may require arithmetic
Note: See TracChangeset
for help on using the changeset viewer.