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

Commits: d5df9cb4 by Laurent at 2020-08-25T14:17:53-04:00 Many changes

- - - - -

3 changed files:

- src/elab.ml - src/serialization.ml - src/serialization_types

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 ^ ".tco" 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

===================================== src/serialization.ml ===================================== @@ -6,40 +6,41 @@ open Util open Prelexer open Serialization_types_j

-module LexpMap = Hashtbl.Make (struct type t = Lexp.lexp let hash = Hashtbl.hash let equal = (==) end) -module SubstMap = Hashtbl.Make (struct type t = Lexp.subst let hash = Hashtbl.hash let equal = (==) end) +type lexp_or_subst = + | Lexp of Lexp.lexp + | Subst of Lexp.subst + +module LexpMap = Hashtbl.Make + (struct type t = lexp_or_subst let hash = Hashtbl.hash let equal = (==) end)

(* Serialization context - HashMap from lexp/subst to the position of the serialized lexp/subst when serialized. - The serialized value is also stored as an optional but should always - contain an element after serialize_lexp finishes. *) + HashMap from lexp/subst to the position of the serialized lexp/subst when + serialized. *) type sctx = { - lexp_refs: (int * Serialization_types_j.lexp option) LexpMap.t; - subst_refs: (int * Serialization_types_j.subst_lexp option) SubstMap.t; + lexp_refs: (int * Serialization_types_j.lexp) LexpMap.t; }

(* Deserialization context *) type dsctx = { - lexp_refs: (int, Lexp.lexp) Hashtbl.t; - subst_refs: (int, Lexp.subst) Hashtbl.t; + lexp_refs: (lexp_or_subst option) array; }

-(* Raised in `sctxToStore` when the option invariant of sctx is false. *) -exception MissingSerializedValue +(* Raised when deserialization fails because the TCO object is corrupted. *) +exception CorruptedSerializedObject

(* Converts from the serialization context to the final, serialization format *) let sctxToStore (sctx: sctx): Serialization_types_j.store = - let toElem (k, (ix, e)) = match e with - | Some x -> (ix, x) - | None -> raise MissingSerializedValue in + let toElem (_, (_, e)) = e in + let cmpIx (_, (i1, _)) (_, (i2, _)) = compare i1 i2 in { - lexp_refs = List.of_seq (Seq.map toElem (LexpMap.to_seq sctx.lexp_refs)); - subst_refs = List.of_seq (Seq.map toElem (SubstMap.to_seq sctx.subst_refs)); + lexp_refs = List.map toElem (* Index of entry == index in the array *) + (List.sort cmpIx (* Sort the entries by their index *) + (List.of_seq (LexpMap.to_seq sctx.lexp_refs))) }

(* Functions serializing lexp and its components. Because of hash consing, sharing must be preserved for lexp and subst. - Other components are serialized as values and copied whenever encountered. (TODO: May be an optimization?) + Other components are serialized as values and copied. *) let serialize_loc (loc: Util.location): Serialization_types_j.location = { file=loc.file; @@ -62,86 +63,133 @@ let rec serialize_pretoken (pretok: Prelexer.pretoken): Serialization_types_j.pr match pretok with | Pretoken (loc, str) -> `Pretoken (serialize_loc loc, str) | Prestring (loc, str) -> `Prestring (serialize_loc loc, str) - | Preblock (loc1, ptks, loc2) -> `Preblock (serialize_loc loc1, List.map serialize_pretoken ptks, serialize_loc loc2) + | Preblock (loc1, ptks, loc2) -> + `Preblock ( serialize_loc loc1 + , List.map serialize_pretoken ptks, serialize_loc loc2)

let rec serialize_sexp (exp: Sexp.sexp): Serialization_types_j.sexp = match exp with - | Block (loc1, ptks, loc2) -> `Block (serialize_loc loc1, List.map serialize_pretoken ptks, serialize_loc loc2) + | Block (loc1, ptks, loc2) -> `Block (serialize_loc loc1 + , List.map serialize_pretoken ptks + , serialize_loc loc2) | Symbol (loc, str) -> `Symbol (serialize_loc loc, str) | String (loc, str) -> `String (serialize_loc loc, str) | Integer (loc, num) -> `Integer (serialize_loc loc, num) | Float (loc, fl) -> `Float (serialize_loc loc, fl) - | Node (s, ss) -> `Node (serialize_sexp s, List.map serialize_sexp ss) + | Node (s, ss) -> `Node ( serialize_sexp s + , List.map serialize_sexp ss)

let rec serialize_subst_lexp (sctx: sctx) (exp: Lexp.subst): Serialization_types_j.subst_lexp_ref = - match SubstMap.find_opt sctx.subst_refs exp with + match LexpMap.find_opt sctx.lexp_refs (Subst exp) with | Some (ix, _) -> ix | None -> - let ix = SubstMap.length sctx.subst_refs in - let addToCtx v = SubstMap.replace sctx.subst_refs exp (ix, Some v); ix in - SubstMap.replace sctx.subst_refs exp (ix, None); - (* let addToCtx v = let k = SubstMap.length sctx.subst_refs in SubstMap.replace sctx.subst_refs exp (k, v); k in *) - match exp with - | Identity db_offset -> addToCtx (`Identity db_offset) - | Cons (lexp, subst, db_offset) -> addToCtx (`Cons (serialize_lexp sctx lexp, serialize_subst_lexp sctx subst, db_offset)) - - and serialize_lexp (sctx: sctx) (exp: Lexp.lexp): int = - match LexpMap.find_opt sctx.lexp_refs exp with + let addToCtx v = + let ix = LexpMap.length sctx.lexp_refs in + LexpMap.replace sctx.lexp_refs (Subst exp) (ix, v); ix in + addToCtx (match exp with + | Identity db_offset -> `SubstIdentity db_offset + | Cons (lexp, subst, db_offset) -> `SubstCons + ( serialize_lexp sctx lexp + , serialize_subst_lexp sctx subst + , db_offset)) + + and serialize_lexp (sctx: sctx) (exp: Lexp.lexp): lexp_ref = + match LexpMap.find_opt sctx.lexp_refs (Lexp exp) with | Some (ix, _) -> ix | None -> - let ix = LexpMap.length sctx.lexp_refs in - LexpMap.replace sctx.lexp_refs exp (ix, None); - let addToCtx v = LexpMap.replace sctx.lexp_refs exp (ix, Some v); ix in - match exp with - | Imm sexp -> addToCtx (`Imm (serialize_sexp sexp)) - | Sort (loc, Stype lexp) -> addToCtx (`Sort (serialize_loc loc, `Stype (serialize_lexp sctx lexp))) - | Sort (loc, StypeOmega) -> addToCtx (`Sort (serialize_loc loc, `StypeOmega)) - | Sort (loc, StypeLevel) -> addToCtx (`Sort (serialize_loc loc, `StypeLevel)) - | SortLevel SLz -> addToCtx (`SortLevel `SLz) - | SortLevel (SLsucc lexp) -> addToCtx (`SortLevel (`SLsucc (serialize_lexp sctx lexp))) - | SortLevel (SLlub (lexp1, lexp2)) -> addToCtx (`SortLevel (`SLlub (serialize_lexp sctx lexp1, serialize_lexp sctx lexp2))) - | Var ((loc, mayName), db_ix) -> addToCtx (`Var ((serialize_loc loc, mayName), db_ix)) - | Builtin (sym, lexp, atts) -> + let addToCtx v = + let ix = LexpMap.length sctx.lexp_refs in + LexpMap.replace sctx.lexp_refs (Lexp exp) (ix, v); ix in + addToCtx (match exp with + | Imm sexp -> + `Imm (serialize_sexp sexp) + + | Sort (loc, Stype lexp) -> + `Sort (serialize_loc loc, `Stype (serialize_lexp sctx lexp)) + + | Sort (loc, StypeOmega) -> + `Sort (serialize_loc loc, `StypeOmega) + + | Sort (loc, StypeLevel) -> + `Sort (serialize_loc loc, `StypeLevel) + + | SortLevel SLz -> + `SortLevel `SLz + + | SortLevel (SLsucc lexp) -> + `SortLevel (`SLsucc (serialize_lexp sctx lexp)) + + | SortLevel (SLlub (lexp1, lexp2)) -> + `SortLevel (`SLlub (serialize_lexp sctx lexp1, serialize_lexp sctx lexp2)) + + | Var ((loc, mayName), db_ix) -> + `Var ((serialize_loc loc, mayName), db_ix) + + | Builtin (sym, lexp, atts) -> let serialize_att ((i, s), lexp) = ((i, s), serialize_lexp sctx lexp) in - addToCtx (`Builtin ( serialize_symbol sym - , serialize_lexp sctx lexp - , Option.map (fun atts -> List.of_seq (Seq.map serialize_att (AttributeMap.to_seq atts))) atts)) + `Builtin ( serialize_symbol sym + , serialize_lexp sctx lexp + , Option.map (fun atts -> List.of_seq + (Seq.map serialize_att + (AttributeMap.to_seq atts))) + atts)

- | Susp (lexp, subst_lexp) -> addToCtx (`Susp (serialize_lexp sctx lexp, serialize_subst_lexp sctx subst_lexp)) - | Let (loc, bindings, lexp) -> - let serialize_binding (vname, lexp, ltype) = (serialize_vname vname, serialize_lexp sctx lexp, serialize_lexp sctx ltype) in - addToCtx (`Let (serialize_loc loc, List.map serialize_binding bindings, serialize_lexp sctx lexp)) + | Susp (lexp, subst_lexp) -> + `Susp (serialize_lexp sctx lexp, serialize_subst_lexp sctx subst_lexp) + + | Let (loc, bindings, lexp) -> + let serialize_binding (vname, lexp, ltype) = + (serialize_vname vname, serialize_lexp sctx lexp, serialize_lexp sctx ltype) in + `Let (serialize_loc loc, List.map serialize_binding bindings, serialize_lexp sctx lexp)

| Arrow (arg_kind, vname, lexp1, a_loc, lexp2) -> - addToCtx (`Arrow ( serialize_arg_kind arg_kind - , serialize_vname vname - , serialize_lexp sctx lexp1 - , serialize_loc a_loc - , serialize_lexp sctx lexp2)) + `Arrow ( serialize_arg_kind arg_kind + , serialize_vname vname + , serialize_lexp sctx lexp1 + , serialize_loc a_loc + , serialize_lexp sctx lexp2) + + | Lambda (arg_kind, vname, lexp1, lexp2) -> + `Lambda ( serialize_arg_kind arg_kind + , serialize_vname vname + , serialize_lexp sctx lexp1 + , serialize_lexp sctx lexp2)

- | Lambda (arg_kind, vname, lexp1, lexp2) -> addToCtx (`Lambda (serialize_arg_kind arg_kind, serialize_vname vname, serialize_lexp sctx lexp1, serialize_lexp sctx lexp2)) | Call (fun_exp, args) -> - let serialize_arg (arg_kind, arg_exp) = (serialize_arg_kind arg_kind, serialize_lexp sctx arg_exp) in - addToCtx (`Call (serialize_lexp sctx fun_exp, List.map serialize_arg args)) + let serialize_arg (arg_kind, arg_exp) = + (serialize_arg_kind arg_kind, serialize_lexp sctx arg_exp) in + `Call (serialize_lexp sctx fun_exp + , List.map serialize_arg args) + | Inductive (loc, sym, l1, l2) -> - let serialize_elem (arg_kind, vname, lexp) = (serialize_arg_kind arg_kind, serialize_vname vname, serialize_lexp sctx lexp) in + let serialize_elem (arg_kind, vname, lexp) = + (serialize_arg_kind arg_kind, serialize_vname vname, serialize_lexp sctx lexp) in let serialize_map (key, e) = (key, List.map serialize_elem e) in - addToCtx (`Inductive ( serialize_loc loc - , serialize_symbol sym - , List.map serialize_elem l1 - , List.of_seq (Seq.map serialize_map (SMap.to_seq l2)) - )) - | Cons (lexp, sym) -> addToCtx (`Cons (serialize_lexp sctx lexp, serialize_symbol sym)) + `Inductive ( serialize_loc loc + , serialize_symbol sym + , List.map serialize_elem l1 + , List.of_seq (Seq.map serialize_map (SMap.to_seq l2)) + ) + | Cons (lexp, sym) -> + `Cons (serialize_lexp sctx lexp, serialize_symbol sym) + | Case (loc, lexp, ltype, cases, default) -> - let serialize_arg (arg_kind, vname) = (serialize_arg_kind arg_kind, serialize_vname vname) in - let serialize_case (k, (loc, args, lexp)) = (k, (serialize_loc loc, List.map serialize_arg args, serialize_lexp sctx lexp)) in - let serialize_default (vname, lexp) = (serialize_vname vname, serialize_lexp sctx lexp) in - addToCtx (`Case ( serialize_loc loc - , serialize_lexp sctx lexp - , serialize_lexp sctx ltype - , List.of_seq (Seq.map serialize_case (SMap.to_seq cases)) - , Option.map serialize_default default)) - | Metavar (meta_id, subst_lexp, vname) -> addToCtx (`Metavar (meta_id, serialize_subst_lexp sctx subst_lexp, serialize_vname vname)) + let serialize_arg (arg_kind, vname) = + (serialize_arg_kind arg_kind, serialize_vname vname) in + let serialize_case (k, (loc, args, lexp)) = + (k, (serialize_loc loc, List.map serialize_arg args, serialize_lexp sctx lexp)) in + let serialize_default (vname, lexp) = + (serialize_vname vname, serialize_lexp sctx lexp) in + `Case ( serialize_loc loc + , serialize_lexp sctx lexp + , serialize_lexp sctx ltype + , List.of_seq (Seq.map serialize_case (SMap.to_seq cases)) + , Option.map serialize_default default) + + | Metavar (meta_id, subst_lexp, vname) -> + `Metavar ( meta_id + , serialize_subst_lexp sctx subst_lexp + , serialize_vname vname))

(* Deserialization functions *) let deserialize_loc (loc: Serialization_types_j.location): Util.location = @@ -163,80 +211,146 @@ let deserialize_arg_kind (arg_kind: Serialization_types_j.arg_kind): Pexp.arg_ki

let rec deserialize_pretoken (pretok: Serialization_types_j.pretoken): Prelexer.pretoken = match pretok with - | `Pretoken (loc, str) -> Pretoken (deserialize_loc loc, str) - | `Prestring (loc, str) -> Prestring (deserialize_loc loc, str) - | `Preblock (loc1, ptks, loc2) -> Preblock (deserialize_loc loc1, List.map deserialize_pretoken ptks, deserialize_loc loc2) + | `Pretoken (loc, str) -> + Pretoken (deserialize_loc loc, str) + | `Prestring (loc, str) -> + Prestring (deserialize_loc loc, str) + | `Preblock (loc1, ptks, loc2) -> + Preblock ( deserialize_loc loc1 + , List.map deserialize_pretoken ptks + , deserialize_loc loc2)

let rec deserialize_sexp (exp: Serialization_types_j.sexp): Sexp.sexp = match exp with - | `Block (loc1, ptks, loc2) -> Block (deserialize_loc loc1, List.map deserialize_pretoken ptks, deserialize_loc loc2) - | `Symbol (loc, str) -> Symbol (deserialize_loc loc, str) - | `String (loc, str) -> String (deserialize_loc loc, str) - | `Integer (loc, num) -> Integer (deserialize_loc loc, num) - | `Float (loc, fl) -> Float (deserialize_loc loc, fl) - | `Node (s, ss) -> Node (deserialize_sexp s, List.map deserialize_sexp ss) - -let rec deserialize_subst_lexp (dsctx: dsctx) (store: Serialization_types_j.store) (ref: Serialization_types_j.subst_lexp_ref): Lexp.subst = - match Hashtbl.find_opt dsctx.subst_refs ref with - | Some subst -> subst - | None -> match List.assoc_opt ref store.subst_refs with - | None -> raise MissingSerializedValue - | Some (`Identity db_offset) -> Identity db_offset - | Some (`Cons (lexp, subst, db_offset)) -> Cons (deserialize_lexp dsctx store lexp, deserialize_subst_lexp dsctx store subst, db_offset) - - and deserialize_lexp (dsctx: dsctx) (store: Serialization_types_j.store) (ref: Serialization_types_j.lexp_ref): Lexp.lexp = - match Hashtbl.find_opt dsctx.lexp_refs ref with - | Some subst -> subst - | None -> Lexp.hc (match List.assoc_opt ref store.lexp_refs with - | None -> raise MissingSerializedValue - | Some (`Imm sexp) -> Imm (deserialize_sexp sexp) - | Some (`Sort (loc, (`Stype lexp))) -> Sort (deserialize_loc loc, Stype (deserialize_lexp dsctx store lexp)) - | Some (`Sort (loc, `StypeOmega)) -> Sort (deserialize_loc loc, StypeOmega) - | Some (`Sort (loc, `StypeLevel)) -> Sort (deserialize_loc loc, StypeLevel) - | Some (`SortLevel `SLz) -> SortLevel SLz - | Some (`SortLevel (`SLsucc lexp)) -> SortLevel (SLsucc (deserialize_lexp dsctx store lexp)) - | Some (`SortLevel (`SLlub (lexp1, lexp2))) -> SortLevel (SLlub (deserialize_lexp dsctx store lexp1, deserialize_lexp dsctx store lexp2)) - | Some (`Var ((loc, mayName), db_ix)) -> Var ((deserialize_loc loc, mayName), db_ix) - | Some (`Builtin (sym, lexp, atts)) -> - let deserialize_att ((i, s), lexp) = ((i, s), deserialize_lexp dsctx store lexp) in - Builtin ( deserialize_symbol sym - , deserialize_lexp dsctx store lexp - , Option.map (fun atts -> AttributeMap.of_seq (Seq.map deserialize_att (List.to_seq atts))) atts) - | Some (`Susp (lexp, subst_lexp)) -> Susp (deserialize_lexp dsctx store lexp, deserialize_subst_lexp dsctx store subst_lexp) - | Some (`Let (loc, bindings, lexp)) -> - let deserialize_binding (vname, lexp, ltype) = (deserialize_vname vname, deserialize_lexp dsctx store lexp, deserialize_lexp dsctx store ltype) in - Let (deserialize_loc loc, List.map deserialize_binding bindings, deserialize_lexp dsctx store lexp) - - | Some (`Arrow (arg_kind, vname, lexp1, a_loc, lexp2)) -> - Arrow ( deserialize_arg_kind arg_kind - , deserialize_vname vname - , deserialize_lexp dsctx store lexp1 - , deserialize_loc a_loc - , deserialize_lexp dsctx store lexp2) - - - | Some (`Inductive (loc, sym, l1, l2)) -> - let deserialize_elem (arg_kind, vname, lexp) = (deserialize_arg_kind arg_kind, deserialize_vname vname, deserialize_lexp dsctx store lexp) in - let deserialize_map (key, e) = (key, List.map deserialize_elem e) in - Inductive ( deserialize_loc loc - , deserialize_symbol sym - , List.map deserialize_elem l1 - , SMap.of_seq (Seq.map deserialize_map (List.to_seq l2)) - ) - - | Some (`Lambda (arg_kind, vname, lexp1, lexp2)) -> Lambda (deserialize_arg_kind arg_kind, deserialize_vname vname, deserialize_lexp dsctx store lexp1, deserialize_lexp dsctx store lexp2) - | Some (`Call (fun_exp, args)) -> - let deserialize_arg (arg_kind, arg_exp) = (deserialize_arg_kind arg_kind, deserialize_lexp dsctx store arg_exp) in - Call (deserialize_lexp dsctx store fun_exp, List.map deserialize_arg args) - - | Some (`Cons (lexp, sym)) -> Cons (deserialize_lexp dsctx store lexp, deserialize_symbol sym) - | Some (`Case (loc, lexp, ltype, cases, default)) -> - let deserialize_arg (arg_kind, vname) = (deserialize_arg_kind arg_kind, deserialize_vname vname) in - let deserialize_case (k, (loc, args, lexp)) = (k, (deserialize_loc loc, List.map deserialize_arg args, deserialize_lexp dsctx store lexp)) in - let deserialize_default (vname, lexp) = (deserialize_vname vname, deserialize_lexp dsctx store lexp) in - Case ( deserialize_loc loc - , deserialize_lexp dsctx store lexp - , deserialize_lexp dsctx store ltype - , SMap.of_seq (Seq.map deserialize_case (List.to_seq cases)) - , Option.map deserialize_default default) - | Some (`Metavar (meta_id, subst_lexp, vname)) -> Metavar (meta_id, deserialize_subst_lexp dsctx store subst_lexp, deserialize_vname vname)) + | `Block (loc1, ptks, loc2) -> + Block (deserialize_loc loc1, List.map deserialize_pretoken ptks, deserialize_loc loc2) + | `Symbol (loc, str) -> + Symbol (deserialize_loc loc, str) + | `String (loc, str) -> + String (deserialize_loc loc, str) + | `Integer (loc, num) -> + Integer (deserialize_loc loc, num) + | `Float (loc, fl) -> + Float (deserialize_loc loc, fl) + | `Node (s, ss) -> + Node (deserialize_sexp s, List.map deserialize_sexp ss) + +let rec lookup_subst (dsctx: dsctx) (index: Serialization_types_j.subst_lexp_ref): Lexp.subst = + match Array.get dsctx.lexp_refs index with + | Some (Subst subst) -> subst + | _ -> raise CorruptedSerializedObject + + and lookup_lexp (dsctx: dsctx) (index: Serialization_types_j.lexp_ref): Lexp.lexp = + match Array.get dsctx.lexp_refs index with + | Some (Lexp lexp) -> lexp + | _ -> raise CorruptedSerializedObject + + and deserialize_lexp (store: Serialization_types_j.store): Lexp.lexp = + let count = List.length store.lexp_refs in + let dsctx: dsctx = { lexp_refs = Array.make count None } in + for i = 0 to count - 1 do + deserialize_lexp_step dsctx store i + done; + lookup_lexp dsctx (count - 1) + + and deserialize_lexp_step (dsctx: dsctx) (store: Serialization_types_j.store) (index: Serialization_types_j.lexp_ref) = + let add_val_to_cxt (v : lexp_or_subst): unit = + Array.set dsctx.lexp_refs index (Some v) in + + add_val_to_cxt (match List.nth store.lexp_refs index with + | `Imm sexp -> Lexp (Lexp.mkImm (deserialize_sexp sexp)) + + | `Sort (loc, (`Stype lexp)) -> + Lexp (Lexp.mkSort (deserialize_loc loc, Stype (lookup_lexp dsctx lexp))) + + | `Sort (loc, `StypeOmega) -> + Lexp (Lexp.mkSort (deserialize_loc loc, StypeOmega)) + + | `Sort (loc, `StypeLevel) -> + Lexp (Lexp.mkSort (deserialize_loc loc, StypeLevel)) + + | `SortLevel `SLz -> + Lexp (Lexp.mkSortLevel SLz) + + | `SortLevel (`SLsucc lexp) -> + Lexp (Lexp.mkSortLevel (Lexp.mkSLsucc (lookup_lexp dsctx lexp))) + + | `SortLevel (`SLlub (lexp1, lexp2)) -> + Lexp (Lexp.mkSortLevel (Lexp.mkSLlub' (lookup_lexp dsctx lexp1, lookup_lexp dsctx lexp2))) + + | `Var ((loc, mayName), db_ix) -> + Lexp (Lexp.mkVar ((deserialize_loc loc, mayName), db_ix)) + + | `Builtin (sym, lexp, atts) -> + let deserialize_att ((i, s), lexp) = ((i, s), lookup_lexp dsctx lexp) in + Lexp (Lexp.mkBuiltin ( deserialize_symbol sym + , lookup_lexp dsctx lexp + , Option.map (fun atts -> + AttributeMap.of_seq + (Seq.map deserialize_att + (List.to_seq atts))) atts)) + + | `Susp (lexp, subst_lexp) -> + Lexp (Lexp.mkSusp (lookup_lexp dsctx lexp) (lookup_subst dsctx subst_lexp)) + + | `Let (loc, bindings, lexp)-> + let deserialize_binding (vname, lexp, ltype) = + (deserialize_vname vname, lookup_lexp dsctx lexp, lookup_lexp dsctx ltype) in + Lexp (Lexp.mkLet ( deserialize_loc loc + , List.map deserialize_binding bindings + , lookup_lexp dsctx lexp)) + + | `Arrow (arg_kind, vname, lexp1, a_loc, lexp2) -> + Lexp (Lexp.mkArrow ( deserialize_arg_kind arg_kind + , deserialize_vname vname + , lookup_lexp dsctx lexp1 + , deserialize_loc a_loc + , lookup_lexp dsctx lexp2)) + + | `Inductive (loc, sym, l1, l2) -> + let deserialize_elem (arg_kind, vname, lexp) = + (deserialize_arg_kind arg_kind, deserialize_vname vname, lookup_lexp dsctx lexp) in + let deserialize_map (key, e) = (key, List.map deserialize_elem e) in + Lexp (Lexp.mkInductive ( deserialize_loc loc + , deserialize_symbol sym + , List.map deserialize_elem l1 + , SMap.of_seq (Seq.map deserialize_map (List.to_seq l2)))) + + | `Lambda (arg_kind, vname, lexp1, lexp2) -> + Lexp (Lexp.mkLambda ( deserialize_arg_kind arg_kind + , deserialize_vname vname + , lookup_lexp dsctx lexp1 + , lookup_lexp dsctx lexp2)) + + | `Call (fun_exp, args) -> + let deserialize_arg (arg_kind, arg_exp) = + (deserialize_arg_kind arg_kind, lookup_lexp dsctx arg_exp) in + Lexp (Lexp.mkCall ( lookup_lexp dsctx fun_exp + , List.map deserialize_arg args)) + + | `Cons (lexp, sym) -> + Lexp (Lexp.mkCons (lookup_lexp dsctx lexp, deserialize_symbol sym)) + + | `Case (loc, lexp, ltype, cases, default) -> + let deserialize_arg (arg_kind, vname) = + (deserialize_arg_kind arg_kind, deserialize_vname vname) in + let deserialize_case (k, (loc, args, lexp)) = + (k, (deserialize_loc loc, List.map deserialize_arg args, lookup_lexp dsctx lexp)) in + let deserialize_default (vname, lexp) = + (deserialize_vname vname, lookup_lexp dsctx lexp) in + Lexp (Lexp.mkCase ( deserialize_loc loc + , lookup_lexp dsctx lexp + , lookup_lexp dsctx ltype + , SMap.of_seq (Seq.map deserialize_case (List.to_seq cases)) + , Option.map deserialize_default default)) + + | `Metavar (meta_id, subst_lexp, vname) -> + Lexp (Lexp.mkMetavar ( meta_id + , lookup_subst dsctx subst_lexp + , deserialize_vname vname)) + + | `SubstIdentity db_offset -> + Subst (Identity db_offset) + + | `SubstCons (lexp, subst, db_offset) -> + Subst (Cons (lookup_lexp dsctx lexp, lookup_subst dsctx subst, db_offset)))

===================================== src/serialization_types ===================================== @@ -1,6 +1,12 @@ +(*Types for serialiation of lexps + Very similar to the types in lexp.ml and sexp.ml, except that recursive + types are replaced with the index of the object pointed to in the + serialization store. + *) +(* TODO: Find way to automatically generate them to reduce duplication *) + type store = { - lexp_refs: (int * lexp) list; - subst_refs: (int * subst_lexp) list; + lexp_refs: lexp list; }

type location = { @@ -39,10 +45,6 @@ type vref = (vname * db_index) type lexp_ref = int

type subst_lexp_ref = int -type subst_lexp = [ - | Identity of db_offset - | Cons of (lexp_ref * subst_lexp_ref * db_offset) -]

type arg_kind = [ Anormal | Aimplicit | Aerasable ]

@@ -66,6 +68,8 @@ type lexp = [ * (string * (location * (arg_kind * vname) list * lexp_ref)) list * (vname * lexp_ref) option) | Metavar of (meta_id * subst_lexp_ref * vname) + | SubstIdentity of db_offset + | SubstCons of (lexp_ref * subst_lexp_ref * db_offset) ]

type sort = [

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/d5df9cb43fa33eb55fc77d0d3490f3b2c5...