swh:1:snp:ca722f838562be139d7880d2b37d9db111694bf0
Tip revision: 52466cf87cc0c8efb6819de5d55f7779a9ba8b5f authored by Antoine Séré on 26 January 2023, 12:09:15 UTC
Incomplete if
Incomplete if
Tip revision: 52466cf
roadmap.ec
(*
module M = {
proc h() = {
@L:
}
proc f() = {
@L1:
}
proc g() = {
@L2:
}
}.
equiv [M.f ~ M.g : pre ==> post | {
(L1, L2) --> assertion
...
}].
*)
(*
- faire un petite exemple qui fixe la syntaxe
- modifier PST
- ecParsetree.ml
- instructions: pinstr
- PFequivF(pre, (f, g), post), labels) -> assert: prhl
- étendre parseur
- ecParser.mly (menhir)
- formule: sform_u [equiv étendu]
- procedures: base_instr [instructions]
- modifier AST
- ecCoreModule.ml
- instructions: instr
- hash-consing + constructeurs / destructeurs
- substitutions (no-op) ?
- ecCoreFol.ml
- equivF[proc] / equivS[stmt]
- adapter typeur
- ecTyping.ml
- trans_form_or_pattern
- transinstr
- étendre environnement avec les labels
- implémeter les règles de la logique (+ parser)
- phl/* [un fichier par tactique]
- exemples
- profits
*)