From 39a112952e328ce52e5f7b08bf18bbadd3fca03f Mon Sep 17 00:00:00 2001 From: Jedidiah Barber Date: Wed, 19 Nov 2025 16:51:08 +1300 Subject: Reification, including Term flattening and Treeification --- src/kompsos.ads | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) (limited to 'src/kompsos.ads') diff --git a/src/kompsos.ads b/src/kompsos.ads index 89ea88b..3164996 100644 --- a/src/kompsos.ads +++ b/src/kompsos.ads @@ -256,6 +256,10 @@ package Kompsos is (This : in out World) return State; + function Take_All + (This : in out World) + return State_Array; + procedure Force (This : in out World; Count : in Positive); @@ -268,6 +272,28 @@ package Kompsos is return Boolean; + -- Reification -- + + function Resolve + (This : in Term; + Subst : in State) + return Term; + + function Resolve_First + (Subst : in State) + return Term; + + function Resolve_First + (Subst : in State; + Name : in String) + return Term; + + function Resolve_First + (Subst : in State; + Name : in Nametag) + return Term; + + -------------------------- @@ -474,6 +500,10 @@ private Actual : Term_Holders.Holder; end record; + function T + (Item : in Variable) + return Term'Class; + function Var (This : in Term'Class) return Variable -- cgit