A 'textbook' unification algorithm

.gitignore

@@ -33,7 +33,7 @@ nia.cache
 nlia.cache
 nra.cache
 native_compute_profile_*.data
-
+.vagrant
 # generated timing files
 *.timing.diff
 *.v.after-timing

dist/vagrant/fedora39-nix/Vagrantfile

@@ -0,0 +1,95 @@
+# -*- mode: ruby -*-
+# vi: set ft=ruby :
+
+# All Vagrant configuration is done below. The "2" in Vagrant.configure
+# configures the configuration version (we support older styles for
+# backwards compatibility). Please don't change it unless you know what
+# you're doing.
+Vagrant.configure("2") do |config|
+  # The most common configuration options are documented and commented below.
+  # For a complete reference, please see the online documentation at
+  # https://docs.vagrantup.com.
+
+  # Every Vagrant development environment requires a box. You can search for
+  # boxes at https://vagrantcloud.com/search.
+  config.vm.box = "generic/fedora39"
+
+
+  config.vm.provider :libvirt do |libvirt|
+    libvirt.cpus = 1
+    libvirt.memory = 12288
+  end
+  # Disable automatic box update checking. If you disable this, then
+  # boxes will only be checked for updates when the user runs
+  # `vagrant box outdated`. This is not recommended.
+  # config.vm.box_check_update = false
+
+  # Create a forwarded port mapping which allows access to a specific port
+  # within the machine from a port on the host machine. In the example below,
+  # accessing "localhost:8080" will access port 80 on the guest machine.
+  # NOTE: This will enable public access to the opened port
+  # config.vm.network "forwarded_port", guest: 80, host: 8080
+
+  # Create a forwarded port mapping which allows access to a specific port
+  # within the machine from a port on the host machine and only allow access
+  # via 127.0.0.1 to disable public access
+  # config.vm.network "forwarded_port", guest: 80, host: 8080, host_ip: "127.0.0.1"
+
+  # Create a private network, which allows host-only access to the machine
+  # using a specific IP.
+  # config.vm.network "private_network", ip: "192.168.33.10"
+
+  # Create a public network, which generally matched to bridged network.
+  # Bridged networks make the machine appear as another physical device on
+  # your network.
+  # config.vm.network "public_network"
+
+  # Share an additional folder to the guest VM. The first argument is
+  # the path on the host to the actual folder. The second argument is
+  # the path on the guest to mount the folder. And the optional third
+  # argument is a set of non-required options.
+  # config.vm.synced_folder "../data", "/vagrant_data"
+  config.vm.provision "file", source: "../../../minuska", destination: "$HOME/minuska-src"
+
+  # Disable the default share of the current code directory. Doing this
+  # provides improved isolation between the vagrant box and your host
+  # by making sure your Vagrantfile isn't accessible to the vagrant box.
+  # If you use this you may want to enable additional shared subfolders as
+  # shown above.
+  # config.vm.synced_folder ".", "/vagrant", disabled: true
+
+  # Provider-specific configuration so you can fine-tune various
+  # backing providers for Vagrant. These expose provider-specific options.
+  # Example for VirtualBox:
+  #
+  # config.vm.provider "virtualbox" do |vb|
+  #   # Display the VirtualBox GUI when booting the machine
+  #   vb.gui = true
+  #
+  #   # Customize the amount of memory on the VM:
+  #   vb.memory = "1024"
+  # end
+  #
+  # View the documentation for the provider you are using for more
+  # information on available options.
+
+  # Enable provisioning with a shell script. Additional provisioners such as
+  # Ansible, Chef, Docker, Puppet and Salt are also available. Please see the
+  # documentation for more information about their specific syntax and use.
+  config.vm.provision "shell", inline: <<-SHELL
+    setenforce 0
+    sh <(curl -L https://nixos.org/nix/install) --daemon
+    echo 'experimental-features = nix-command flakes' >> /etc/nix/nix.conf
+    #dnf update
+    #dnf install -y opam ocaml-dune
+  SHELL
+
+  config.vm.provision "shell", privileged: false, inline: <<-SHELL
+    #opam init --auto-setup
+    #eval $(opam env)
+    #opam pin add coq 8.19.0
+    #opam repo add coq-released https://coq.inria.fr/opam/released
+    #opam install coq-equations coq-stdpp core core_unix menhir
+  SHELL
+
+end

flake.nix

@@ -4,9 +4,11 @@
   inputs = {
     nixpkgs.url = "github:NixOs/nixpkgs";
     flake-utils.url = "github:numtide/flake-utils";
+    vscoq.url = "github:coq-community/vscoq";
+    vscoq.inputs.nixpkgs.follows = "nixpkgs";
    };
 
-  outputs = { self, nixpkgs, flake-utils }: (
+  outputs = { self, nixpkgs, flake-utils, vscoq }: (
     flake-utils.lib.eachDefaultSystem (system:
       let
 
@@ -17,6 +19,9 @@
            let stdpp = coqPackages.stdpp; in
            let coqLibraries = [
               coqPackages.equations
+              coqPackages.QuickChick
+              # TODO remove, we will not use this
+              #coqPackages.CoLoR
               stdpp
            ]; in
            let bothNativeAndOtherInputs = [
@@ -169,7 +174,11 @@
             in
               pkgs.mkShell {
                 inputsFrom = [minuska];
-                packages = [minuska.coqPackages.coq-lsp minuska.coqPackages.coqide];
+                packages = [
+                  minuska.coqPackages.coq-lsp 
+                  minuska.coqPackages.coqide 
+                  vscoq.packages.${system}.vscoq-language-server-coq-8-19
+                ];
               };
 
           # For using Minuska

minuska/_CoqProject

@@ -30,3 +30,4 @@ theories/dt.v
 theories/interp_loop.v
 theories/example.v
 theories/default_everything.v
+theories/symex.v

minuska/theories/dt.v

@@ -1401,7 +1401,6 @@ Proof.
         {
             unfold cmmatch in H.
             destruct H as [j [pv [H1 H2]]].
-            Search lookup nil.
             inversion H1.
         }
         {