Laurent Huberdeau pushed to branch laurent/elab_cache at Stefan / Typer

Commits: a1e36f7f by Laurent at 2020-08-25T10:27:21-04:00 Use tco instead of json for serialized lexp files

- - - - - 1cb32a06 by Laurent at 2020-08-25T14:16:55-04:00 Many changes

- - - - -

1 changed file:

- src/elab.ml

Changes:

===================================== src/elab.ml ===================================== @@ -1802,14 +1802,16 @@ let sform_load usr_elctx loc sargs ot = let file_string = String.concat "" (read_lines file_path) in let file_hash = Hashtbl.hash file_string in let cached_file_name = file_name ^ string_of_int file_hash in - let cached_file_path = "cache/" ^ cached_file_name ^ ".json" in + (* Different serialized value if in pervasive *) + let cached_file_path = if !in_pervasive + then "cache/" ^ cached_file_name ^ ".ptco" + else "cache/" ^ cached_file_name ^ ".tco" in

if Sys.file_exists cached_file_path then let store_str = String.concat "" (read_lines cached_file_path) in let store = Serialization_types_j.store_of_string store_str in - let dsctx: Serialization.dsctx = { lexp_refs = Hashtbl.create 1000; subst_refs = Hashtbl.create 1000 } in - let res = Serialization.deserialize_lexp dsctx store 0 in - (res, Lazy) + let tuple = Serialization.deserialize_lexp store in + (tuple, Lazy) else

(* get lexp_context *) @@ -1834,10 +1836,8 @@ let sform_load usr_elctx loc sargs ot = else (Lexp.mkSusp tuple (S.shift (usr_len - dflt_len))) in

- (* Cache result *) - let sctx: Serialization.sctx = { - lexp_refs = Serialization.LexpMap.create 1000; - subst_refs = Serialization.SubstMap.create 1000 } in + (* Save result to disk *) + let sctx: Serialization.sctx = { lexp_refs = Serialization.LexpMap.create 1000 } in let _ = Serialization.serialize_lexp sctx tuple' in

let store = Serialization.sctxToStore sctx in

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/1718b1111f11cc933aaa67e449e47c492...