Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
why3
why3
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 119
    • Issues 119
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 16
    • Merge Requests 16
  • Operations
    • Operations
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
  • Why3
  • why3why3
  • Issues
  • #377

Closed
Open
Opened Aug 22, 2019 by DAILLER Sylvain@sdaillerDeveloper

Why3 should not introduce spaces in identifiers

Spaces are introduced in identifiers in some cases. This makes it impossible for the user to use these identifiers in arguments of transformations.

An example with records is the following:

use int.Int

type r = {a : int; b : int}

let f (x y: r): bool
  ensures {x.a = y.a}
  =
  true

To explicitly show the problem use the following transformations: introduce_premises destruct_term x assert (x2 = mk r x1 x)

@marche suggest to use tick ' instead of space because the user would still not be able to define those in .mlw file but they would be able to use them. Here, the result would be something along the lines of r'mk.

Note that spaces also appear in the names of goals: they could be removed in favor of ' too. For example: f'VC.

On this issue, I will try to make a MR with the simple replacement of mk with 'mk to see if it could work. Note that I also expect to change accordingly any code that would recognize a record by looking if its name begins with mk .

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: why3/why3#377