au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Same name for type constructor and variant constructor breaks antiquoted C #286

Open amosr opened 5 years ago

amosr commented 5 years ago

Name overlap: Error as variant constructor and type constructor as in following example:

type R e a = < Error e | Ok a >
type Error = <ErrorEOF | ErrorFull | ErrorEtc U32>

xxx : R Error () -> R Error ()
xxx y =
 y
 | Error e -> Error e
 | Ok a -> Ok a

This gives an error in the generated antiquoted C

cogent FileFFI.cogent -g -Od -ogenerated --fno-fncall-as-macro --ffunc-purity-attr \
                --infer-c-types="" \
                --Wno-warn --infer-c-funcs="main.ac" \
                --cpp-args="\$CPPIN -o \$CPPOUT -E -P -I. -I/home/amosr/proj/cogent/cogent/.cabal-sandbox/share/x86_64-linux-ghc-8.6.3/cogent-2.9.0.0/include/ -I/home/amosr/proj/cogent/cogent/.cabal-sandbox/share/x86_64-linux-ghc-8.6.3/cogent-2.9.0.0/include//gum/anti -std=gnu99" \
                --ext-types=types.cfg \
                --entry-funcs=entrypoints.cfg \

Parsing...
Resolving dependencies...
Typechecking...
Desugaring and typing...
Normalising...ANF
Re-typing NF...
Simplifying...
Skipped
Monomorphising...
Re-typing monomorphic AST...
Generating C code...
  > Writing to file: ./generated.h
  > Writing to file: ./generated.c
Generating glue code...
Preprocessing C files...
  > Writing to file: ./main_pp.ac
Glue code (functions) generation failed: 
Error: Failed to parse C: ./main_pp.ac:63:44:
    parse error on `Error'
Compilation failed!