Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make LVar, PVar, Loc and ALoc opaque types #332

Draft
wants to merge 4 commits into
base: master
Choose a base branch
from

Conversation

N1ark
Copy link
Contributor

@N1ark N1ark commented Jan 22, 2025

  • Merge the modules ALoc, LVar and Var into the Id module that handles string IDs.
    • Defined an id as type +'a t = string, which is opaque to outside modules.
    • Defines the polymorphic variants lvar, var, loc and aloc.
    • Defines the aliases any_var = [ var | lvar ], any_loc = [ loc | aloc ], substable = [ lvar | var | aloc ], and any = [ lvar | var | loc | aloc ].
    • Define the modules ALoc, LVar, Var and Loc that contain allocation methods, and from/to string functions. Currently the from/to string conversion doesn't do any checking.
  • Replace all instances of string LVars with Id.lvar Id.t: Expr.LVar,Exists,ForAll SLCmd.Fold,Unfold, Cmd.Call (for bindings), Pred.pred_definitions, Lemma.lemma_existentials,Spec.ss_label.
  • Use the new Id type in Gil_syntax:
    • Relevant changes are in GillianCore/GIL_Syntax/Gil_syntax.mli
    • Replace all instances of string Vars with Id.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_params
    • Replace all instances of mixed LVars and Vars with Id.any_var Id.t: SLCmd.ApplyLem,SepAssert,Invariant,Consume.
  • Whenever possible, replaced uses of SS (string set) with a typed set (e.g. ALoc.Set).
  • Updated WISL, C, C2, JS and transformers to match these types. For JS in particular, I tried making it work with the least amount of changes, so there might be odd places where we jump between raw strings and typed IDs quite a bit; otherwise I would've had to rework too much code.

Resolves #7

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Types modeled as strings should be opaque
1 participant