package forester
A tool for tending mathematical forests
Install
dune-project
Dependency
Authors
Maintainers
Sources
5.0.tar.gz
md5=24f4aed96a8b8af33aba13fba66f1b37
sha512=d36b896aca11858bb4a00fc704c16cc27a1f197bdb3e479d6132fd70f70d67d7158096285cb0b6fb00db14417f0f822cc27fe65d82f0971e42378fd8271ce573
doc/src/forester.core/Datalog_eval.ml.html
Source file Datalog_eval.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
(* * SPDX-FileCopyrightText: 2024 The Forester Project Contributors * * SPDX-License-Identifier: GPL-3.0-or-later *) open Forester_prelude module Dx = Datalog_expr module D = Datalog_engine let eval_var (var : Dx.var) = D.mk_var (D.var_of_string var) let eval_const (vtx : Vertex.t) = D.mk_const vtx let eval_term : _ Dx.term -> D.term = function | Dx.Var var -> eval_var var | Dx.Const c -> eval_const c let eval_prop (prop : _ Dx.prop) : D.literal = let args = List.map eval_term prop.args in D.mk_literal prop.rel args let eval_premises = List.map eval_prop let eval_sequent (sequent : _ Dx.sequent) : D.clause = D.mk_clause (eval_prop sequent.conclusion) @@ eval_premises sequent.premises let eval_script : _ Dx.script -> D.clause list = List.map eval_sequent let run_query (db : D.db) (query : (string, Vertex.t) Dx.query) : Vertex_set.t = let answers = D.ask db ~neg: (eval_premises query.negatives) [|D.var_of_string query.var|] @@ eval_premises query.positives in Vertex_set.of_list @@ let@ answer = List.map @~ D.list_of_answers answers in answer.(0)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>