Make LVar, PVar, Loc and ALoc opaque types #332
Draft
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
ALoc,LVarandVarinto theIdmodule that handles string IDs.type +'a t = string, which is opaque to outside modules.lvar,var,locandaloc.any_var = [ var | lvar ],any_loc = [ loc | aloc ],substable = [ lvar | var | aloc ], andany = [ lvar | var | loc | aloc ].ALoc,LVar,VarandLocthat contain allocation methods, and from/to string functions. Currently the from/to string conversion doesn't do any checking.Id.lvar Id.t:Expr.LVar,Exists,ForAllSLCmd.Fold,Unfold,Cmd.Call(for bindings),Pred.pred_definitions,Lemma.lemma_existentials,Spec.ss_label.GillianCore/GIL_Syntax/Gil_syntax.mliId.var Id.t:Expr.PVar,LCmd.FreshSVar,Cmd.Assignement,LAction,Call,ECall,Apply,Arguments,PhiAssignement,Pred.pred_params,Lemma.lemma_params,Macro.macro_params,Spec.spec_params,BiSpec.bi_spec_params,Proc.proc_paramsId.any_var Id.t:SLCmd.ApplyLem,SepAssert,Invariant,Consume.SS(string set) with a typed set (e.g.ALoc.Set).Resolves #7