Skip to content

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