Commit Graph

2860 Commits

Author SHA1 Message Date
Denis Merigoux
5cbab517db
Fixing nix updating (#367) 2022-12-12 17:39:35 +01:00
adelaett
c155e18fda
unpinning bindlib, cmdliner, re, ppx_yojson_conv 2022-12-12 11:55:22 +01:00
Denis Merigoux
90291c55c2
Fix issue 362 with wrong encoding of context variables that are functions (#363) 2022-12-07 19:22:01 +01:00
Denis Merigoux
da1350f581
Simplify unboxing 2022-12-07 17:44:14 +01:00
Denis Merigoux
619461dba8
Merge branch 'master' into fix_362 2022-12-07 15:32:08 +01:00
Denis Merigoux
e9fd40dddd
Hotfix for CI 2022-12-06 18:11:40 +01:00
Denis Merigoux
07edff2cd2
Add a disambiguation pass to resolve structure field accesses (#361) 2022-12-06 17:33:58 +01:00
Denis Merigoux
e448a1a1b4
Fix 362 (was harder than expected and unit tests helped catch subsequent encoding bugs!) 2022-12-02 16:42:29 +01:00
Denis Merigoux
eee9946847
Fix extra error on empty 2022-12-02 12:07:26 +01:00
Denis Merigoux
6523181ec7
Wrote unit tests before fix 2022-12-01 18:14:03 +01:00
Louis Gesbert
4ee4a96ac7 Remove *all* struct field access qualifiers in catala code
They are no longer needed \o/
2022-11-28 16:42:02 +01:00
Louis Gesbert
8960e5dbbc Add typing-based disambiguation pass after desugaring
Some typing errors are changed a little, because they get triggered during the
typing of the disambiguation pass, which does not specify the expected return
type (it's an expected invariant that it should not be needed for
disambiguation).

It would be possible to still specify these types during disambiguation just to
get the same errors, but since the newer ones don't appear to be clearly worse
at the moment, it has not been done.
2022-11-28 16:38:09 +01:00
Louis Gesbert
b3ee503b12 Scopelang.From_desugared: some cleanup/reformat 2022-11-28 16:38:09 +01:00
Louis Gesbert
01957c6698 Desugaring: inline the Fold predicate
the intermediate variable made it much harder to type.
2022-11-28 16:38:09 +01:00
Louis Gesbert
3f2aa19e97 Add ambiguous StructAccess for desugared
to be resolved in scopelang
2022-11-28 16:38:09 +01:00
Louis Gesbert
c92fe5e72d Fix underline of code errors when code contains utf8 2022-11-28 16:38:09 +01:00
Louis Gesbert
af2f5dbe19 Tweak error message location printing 2022-11-28 16:38:09 +01:00
Louis Gesbert
9fc4c0c10c Define Catala_utils.String as an overlay to stdlib string 2022-11-28 16:38:09 +01:00
Louis Gesbert
660e5775de Rename utils to catala_utils 2022-11-28 16:38:09 +01:00
Louis Gesbert
b329afbbdb Rename all Map/Set calls accordingly
This is just a bunch of `sed` calls:
```shell
sed -i 's/ScopeSet/ScopeName.Set/g' compiler/**/*.ml*
sed -i 's/ScopeMap/ScopeName.Map/g' compiler/**/*.ml*
sed -i 's/StructMap/StructName.Map/g' compiler/**/*.ml*
sed -i 's/StructSet/StructName.Set/g' compiler/**/*.ml*
sed -i 's/EnumMap/EnumName.Map/g' compiler/**/*.ml*
sed -i 's/EnumSet/EnumName.Set/g' compiler/**/*.ml*
sed -i 's/StructFieldName/StructField/g' compiler/**/*.ml*
sed -i 's/StructFieldMap/StructField.Map/g' compiler/**/*.ml*
sed -i 's/StructFieldSet/StructField.Set/g' compiler/**/*.ml*
sed -i 's/EnumConstructorMap/EnumConstructor.Map/g' compiler/**/*.ml*
sed -i 's/EnumConstructorSet/EnumConstructor.Set/g' compiler/**/*.ml*
sed -i 's/RuleMap/RuleName.Map/g' compiler/**/*.ml*
sed -i 's/RuleSet/RuleName.Set/g' compiler/**/*.ml*
sed -i 's/LabelMap/LabelName.Map/g' compiler/**/*.ml*
sed -i 's/LabelSet/LabelName.Set/g' compiler/**/*.ml*
sed -i 's/ScopeVarMap/ScopeVar.Map/g' compiler/**/*.ml*
sed -i 's/ScopeVarSet/ScopeVar.Set/g' compiler/**/*.ml*
sed -i 's/SubScopeNameMap/SubScopeName.Map/g' compiler/**/*.ml*
sed -i 's/SubScopeNameSet/SubScopeName.Set/g' compiler/**/*.ml*
```

... and reformat
2022-11-28 16:38:09 +01:00
Louis Gesbert
0030fac7c4 Remove previous set/map definitions 2022-11-28 16:38:09 +01:00
Louis Gesbert
206a24a3e1 Factorise definitions of set and maps for uids 2022-11-28 16:38:09 +01:00
Louis Gesbert
8a4462f6cc Name resolution: small reformatting 2022-11-28 16:38:09 +01:00
Denis Merigoux
d7b9396e87
Correct lines 2022-11-24 15:17:00 +01:00
Louis Gesbert
4f059883c1
Uniformise naming of conversion modules across compilation passes (#358) 2022-11-23 18:53:50 +01:00
Louis Gesbert
47799ea24f Uniform naming of conversion modules across compilation passes 2022-11-22 12:08:18 +01:00
Louis Gesbert
6ecca5c664
AST refactoring (#356) 2022-11-22 11:08:11 +01:00
Louis Gesbert
4dfb4ab44f Add some more doc for Expr.shallow_fold and Expr.map_gather 2022-11-21 17:54:17 +01:00
Louis Gesbert
a5ea9451bc Fix extra spacing in struct printer 2022-11-21 17:11:53 +01:00
Louis Gesbert
4ae392c900 AST refactoring
Many changes got bundled in here and would be too tedious to separate.

Closes #330

See changes in `shared_ast/definitions.ml` to check the main point.

- the biggest change is a modification of the struct and enum types in
  expressions: they are now stored as `Map`s throughout passes, and no longer
  converted to indexed lists after scopelang. Their accessors are also changed,
  and tuples only exist in Lcalc (they're used for closure conversion).

  This implied adding some more information in the contexts, to keep the mapping
  between struct fields and scope output variables. It should also be much more
  robust (no longer relying on assumptions upon different orderings).

- another very pervasive change is more cosmetic: the rewrite of the main AST to
  use inline records, labelling individual subfields.

- moved the checks for correct definitions and accesses of structures from
  `Scope_to_dcalc` to `Typing`

- defining some new shallow iterators in module `Shared_ast.Expr`, and
  factorising a few same-pass rewriting functions accordingly (closure
  conversion, optimisations, etc.)

- some smaller style improvements (ensuring we use the proper compare/equal
  functions instead of `=` in a few `when` closes, for example)
2022-11-17 18:16:09 +01:00
Louis Gesbert
8d7f2152a6 Fill in lambda types when doing type inference 2022-11-17 17:47:24 +01:00
Denis Merigoux
4391cd2a1e
Merge branch 'master' into afromher_334 2022-11-17 15:31:29 +01:00
Denis Merigoux
35e606f155
Do not duplicate the tracking of types of free variables in verification backend (#355) 2022-11-17 15:30:51 +01:00
Aymeric Fromherz
1d0871e65c format 2022-11-16 22:28:20 +01:00
Aymeric Fromherz
cfba9d456a Merge branch 'afromher_verif' into afromher_334 2022-11-16 22:16:11 +01:00
Aymeric Fromherz
16c9bae810 cleanup unused var/module errors 2022-11-16 22:13:14 +01:00
Aymeric Fromherz
fe9ef4f8cb Remove map of free_vars_typ from VC generation 2022-11-16 22:08:07 +01:00
Aymeric Fromherz
5a5003b22d Do not pass free_vars to make_context 2022-11-16 21:59:48 +01:00
Aymeric Fromherz
0ccf7da89a Remove ctx_var from Z3 backend context 2022-11-16 21:57:26 +01:00
Aymeric Fromherz
1343f9e1f6 Leverage typed information embedded in expressions to remove uses of the ctx_var map 2022-11-16 21:55:31 +01:00
Aymeric Fromherz
5c19bdc0db Store typ in z3_vars map 2022-11-16 21:52:14 +01:00
Aymeric Fromherz
43fa3ba550 Start removing ctx_var 2022-11-16 21:36:21 +01:00
Catala nix updated
f7fd02266e update lock files 2022-11-14 00:24:07 +00:00
Aymeric Fromherz
e37ad1de44 Reset tests 2022-11-08 22:28:02 +01:00
Aymeric Fromherz
63572b6963 Add bad test for assertions 2022-11-08 22:27:17 +01:00
Aymeric Fromherz
4af44fb519 Add debug info about encoded assertions 2022-11-08 22:25:07 +01:00
Aymeric Fromherz
c4756c485c WIP: Encoding assertions to Z3 2022-11-08 22:09:35 +01:00
Aymeric Fromherz
b443174033 Better handling of assertions in conditions.ml 2022-11-08 22:09:21 +01:00
Aymeric Fromherz
fee9533b87 Add local asserts to each generated vc 2022-11-08 21:51:56 +01:00
Aymeric Fromherz
3c478148e1 Basic infrastructure for collecting assertions 2022-11-08 20:55:40 +01:00