package acgtk

  1. Overview
  2. Docs

This module implements the reduction from ACG signatures and lexicons to datalog programs

Parameters

Signature

generate_and_add_rule ~abs_cst ~obj_princ_type ~obj_typing_env prog abs_sig obj_sig returns a pair (r,prog') where:

  • r is the generated rule
  • prog' is prog where the rule r has been added
  • abs_cst is the abstract constant from the abstract signature abs_sig that triggers the rule generation
  • obj_princ_type is the principal type of the image by the lexicon of abs_cst
  • obj_typing_env is its typing environment. The latter maps the position of the object constants in the realisation of abs_cst to a pair (t,ty) where t is the object constant itself, and ty the type associated by the principal typing environment.
  • prog is the current datalog program
  • abs_sig and obj_sig are the abstract signature and the object signature of some ACG.

edb_and_query ~obj_term ~obj_type ~obj_typing_env ~dist_type prog ~abs_sig ~obj_sig returns a pair (q,prog') where:

  • q is the predicate corresponding to the query generated by the object term obj_term to parse
  • prog' is prog where the extensional database resulting from the reduction of the object term obj_term
  • obj_type is the principal type of obj_term
  • obj_typing_env is its typing environment. The latter maps the position of the object constants in the realisation of abs_cst to a pair (t,ty) where t is the object constant itself, and ty the type associated by the principal typing environment.
  • dist_type is the distinguished type of the ACG
  • prog is the current datalog program
  • abs_sig and obj_sig are the abstract signature and the object signature of some ACG.
OCaml

Innovation. Community. Security.