gillian » Gillian » Command_line » Act_console » Make » Gil_parsing

Parameter Make.Gil_parsing

type annot = PC.Annot.t

type parsing_result = {

1. labeled_prog : (annot, string) Gil_syntax.Prog.t;
   (*

   The parsed program

   *)
2. init_data : Yojson.Safe.t;
   (*

   Will be `Null if no init_data is parsed

   *)

}

val parse_eprog_from_file : string -> parsing_result Utils.Gillian_result.t

Takes a path to a file and returns the parsed GIL program with its global environment.

val parse_eprog_from_string : string -> parsing_result Utils.Gillian_result.t

Takes a string containing a GIL program and parses it.

val eprog_to_prog :
  ?prog_path:string ->
  other_imports:
    (string
     * (string ->
     (annot, string) Gil_syntax.Prog.t Utils.Gillian_result.t))
      list ->
  (annot, string) Gil_syntax.Prog.t ->
  (annot, int) Gil_syntax.Prog.t Utils.Gillian_result.t

Converts a string-labelled Prog.t to an index-labelled Prog.t, resolving the imports in the meantime. The parameter other_imports is an association list that maps extensions to a parser and compiler. For example, it is possible to import a JSIL file in a GIL program using import "file.jsil";. In order to do so, the other_imports list should contain the tuple ("jsil", parse_and_compile_jsil_file) where parse_and_compile_jsil_file is a function that takes a file path, parses the file as a JSIL program, and compiles this to a GIL program.

val cache_labelled_progs :
  (string * (annot, string) Gil_syntax.Prog.t) list ->
  unit

Caches a mapping from the output GIL filepaths to the corresponding sring-labelled GIL programs. Can be called before eprog_to_prog in order to allow the import-resolving mechanism to work without having to first write the GIL programs to file.

val parse_literal :
  Stdlib.Lexing.lexbuf ->
  Gil_syntax.Literal.t Utils.Gillian_result.t

Parses a Literal.t from a lexbuf; raises Failure if parsing fails.

val parse_expression :
  Stdlib.Lexing.lexbuf ->
  Gil_syntax.Expr.t Utils.Gillian_result.t

Parses a Expr.t from a lexbuf; raises Failure if parsing fails.