package acgtk

  1. Overview
  2. Docs
package acgtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module MagicRewriting.RewritingSource

Module to rewrite program and derivations.

Log is the log module for Rewriting

Sourcetype magic_context = {
  1. predicates_from_magic : Magic.extra_pred_type ASPred.PredIdMap.t;
    (*

    A record of the predicates addded by the magic rewriting

    *)
  2. unique_to_original_rules_ids_map : (int * int) DatalogLib.Datalog_AbstractSyntax.RuleIdMap.t;
    (*

    A correspondance beetwen the rule ids of the original program and the preproccess program.

    The key is the rule id of the preprocess program and the value the corresponding id in the original program and the number of idb predicates (used to transform premises)

    *)
  3. magic_to_unique_rule_ids_map : int DatalogLib.Datalog_AbstractSyntax.RuleIdMap.t;
    (*

    A correspondance beetwen the rule ids of the preprocess program and the magic program.

    *)
  4. adorn_to_unadorm_pred_ids_map : ASPred.pred_id ASPred.PredIdMap.t;
    (*

    A correspondace beetween the id of an adorned predicate and the id of the original predicate.

    *)
  5. unique_binding_program : ASProg.program;
}

Record to rewrite proof

Sourceval rewrite_programs : ?msg:string -> ASProg.program -> (ASProg.program * magic_context) QueryMap.t

rewrite_programs program Build a map of magic programs for every predicate that occur in the program

get_program query query_map Returns the good magic program for the query and updates this program with the seed in it.

rewrite_derivations derivations magic_context Rewrites derivations from a magic program to the corresponding derivations in the original program.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct