Deducteam · gares · Jun 9, 2020 · Jun 9, 2020 · Jun 9, 2020 · Jan 27, 2023
diff --git a/dune-workspace b/dune-workspace
diff --git a/lambdap.elpi b/lambdap.elpi
diff --git a/lambdapi.opam b/lambdapi.opam
@@ -62,6 +62,7 @@ depends: [
   "cmdliner" {>= "1.1.0"}
   "stdlib-shims" {>= "0.1.0"}
   "odoc" {with-doc}
+  "elpi" { >= "1.16.6" & < "1.17.0" }
 ]
 build: [
   ["dune" "subst"] {dev}

diff --git a/out/Coq__Arith__Arith__base.dk.gz b/out/Coq__Arith__Arith__base.dk.gz
diff --git a/out/Coq__Arith__Between.dk.gz b/out/Coq__Arith__Between.dk.gz
diff --git a/out/Coq__Arith__Compare__dec.dk.gz b/out/Coq__Arith__Compare__dec.dk.gz
diff --git a/out/Coq__Arith__EqNat.dk.gz b/out/Coq__Arith__EqNat.dk.gz
diff --git a/out/Coq__Arith__Factorial.dk.gz b/out/Coq__Arith__Factorial.dk.gz
diff --git a/out/Coq__Arith__Gt.dk.gz b/out/Coq__Arith__Gt.dk.gz
diff --git a/out/Coq__Arith__Le.dk.gz b/out/Coq__Arith__Le.dk.gz
diff --git a/out/Coq__Arith__Lt.dk.gz b/out/Coq__Arith__Lt.dk.gz
diff --git a/out/Coq__Arith__Minus.dk.gz b/out/Coq__Arith__Minus.dk.gz
diff --git a/out/Coq__Arith__Mult.dk.gz b/out/Coq__Arith__Mult.dk.gz
diff --git a/out/Coq__Arith__PeanoNat.dk.gz b/out/Coq__Arith__PeanoNat.dk.gz
diff --git a/out/Coq__Arith__Peano__dec.dk.gz b/out/Coq__Arith__Peano__dec.dk.gz
diff --git a/out/Coq__Arith__Plus.dk.gz b/out/Coq__Arith__Plus.dk.gz
diff --git a/out/Coq__Arith__Wf__nat.dk.gz b/out/Coq__Arith__Wf__nat.dk.gz
diff --git a/out/Coq__Bool__Bool.dk.gz b/out/Coq__Bool__Bool.dk.gz
diff --git a/out/Coq__Bool__BoolEq.dk.gz b/out/Coq__Bool__BoolEq.dk.gz
diff --git a/out/Coq__Bool__DecBool.dk.gz b/out/Coq__Bool__DecBool.dk.gz
diff --git a/out/Coq__Bool__IfProp.dk.gz b/out/Coq__Bool__IfProp.dk.gz
diff --git a/out/Coq__Classes__CMorphisms.dk.gz b/out/Coq__Classes__CMorphisms.dk.gz
diff --git a/out/Coq__Classes__CRelationClasses.dk.gz b/out/Coq__Classes__CRelationClasses.dk.gz
diff --git a/out/Coq__Classes__Equivalence.dk.gz b/out/Coq__Classes__Equivalence.dk.gz
diff --git a/out/Coq__Classes__Init.dk.gz b/out/Coq__Classes__Init.dk.gz
diff --git a/out/Coq__Classes__Morphisms.dk.gz b/out/Coq__Classes__Morphisms.dk.gz
diff --git a/out/Coq__Classes__Morphisms__Prop.dk.gz b/out/Coq__Classes__Morphisms__Prop.dk.gz
diff --git a/out/Coq__Classes__RelationClasses.dk.gz b/out/Coq__Classes__RelationClasses.dk.gz
diff --git a/out/Coq__Classes__SetoidTactics.dk.gz b/out/Coq__Classes__SetoidTactics.dk.gz
diff --git a/out/Coq__Init__Datatypes.dk.gz b/out/Coq__Init__Datatypes.dk.gz
diff --git a/out/Coq__Init__Decimal.dk.gz b/out/Coq__Init__Decimal.dk.gz
diff --git a/out/Coq__Init__Logic.dk.gz b/out/Coq__Init__Logic.dk.gz
diff --git a/out/Coq__Init__Logic__Type.dk.gz b/out/Coq__Init__Logic__Type.dk.gz
diff --git a/out/Coq__Init__Nat.dk.gz b/out/Coq__Init__Nat.dk.gz
diff --git a/out/Coq__Init__Notations.dk.gz b/out/Coq__Init__Notations.dk.gz
diff --git a/out/Coq__Init__Peano.dk.gz b/out/Coq__Init__Peano.dk.gz
diff --git a/out/Coq__Init__Prelude.dk.gz b/out/Coq__Init__Prelude.dk.gz
diff --git a/out/Coq__Init__Specif.dk.gz b/out/Coq__Init__Specif.dk.gz
diff --git a/out/Coq__Init__Tactics.dk.gz b/out/Coq__Init__Tactics.dk.gz
diff --git a/out/Coq__Init__Tauto.dk.gz b/out/Coq__Init__Tauto.dk.gz
diff --git a/out/Coq__Init__Wf.dk.gz b/out/Coq__Init__Wf.dk.gz
diff --git a/out/Coq__Logic__Decidable.dk.gz b/out/Coq__Logic__Decidable.dk.gz
diff --git a/out/Coq__Logic__EqdepFacts.dk.gz b/out/Coq__Logic__EqdepFacts.dk.gz
diff --git a/out/Coq__Logic__Eqdep__dec.dk.gz b/out/Coq__Logic__Eqdep__dec.dk.gz
diff --git a/out/Coq__Logic__ProofIrrelevanceFacts.dk.gz b/out/Coq__Logic__ProofIrrelevanceFacts.dk.gz
diff --git a/out/Coq__Numbers__NatInt__NZAdd.dk.gz b/out/Coq__Numbers__NatInt__NZAdd.dk.gz
diff --git a/out/Coq__Numbers__NatInt__NZAddOrder.dk.gz b/out/Coq__Numbers__NatInt__NZAddOrder.dk.gz
diff --git a/out/Coq__Numbers__NatInt__NZAxioms.dk.gz b/out/Coq__Numbers__NatInt__NZAxioms.dk.gz
diff --git a/out/Coq__Numbers__NatInt__NZBase.dk.gz b/out/Coq__Numbers__NatInt__NZBase.dk.gz
diff --git a/out/Coq__Numbers__NatInt__NZBits.dk.gz b/out/Coq__Numbers__NatInt__NZBits.dk.gz
diff --git a/out/Coq__Numbers__NatInt__NZDiv.dk.gz b/out/Coq__Numbers__NatInt__NZDiv.dk.gz
diff --git a/out/Coq__Numbers__NatInt__NZGcd.dk.gz b/out/Coq__Numbers__NatInt__NZGcd.dk.gz
diff --git a/out/Coq__Numbers__NatInt__NZLog.dk.gz b/out/Coq__Numbers__NatInt__NZLog.dk.gz
diff --git a/out/Coq__Numbers__NatInt__NZMul.dk.gz b/out/Coq__Numbers__NatInt__NZMul.dk.gz
diff --git a/out/Coq__Numbers__NatInt__NZMulOrder.dk.gz b/out/Coq__Numbers__NatInt__NZMulOrder.dk.gz
diff --git a/out/Coq__Numbers__NatInt__NZOrder.dk.gz b/out/Coq__Numbers__NatInt__NZOrder.dk.gz
diff --git a/out/Coq__Numbers__NatInt__NZParity.dk.gz b/out/Coq__Numbers__NatInt__NZParity.dk.gz
diff --git a/out/Coq__Numbers__NatInt__NZPow.dk.gz b/out/Coq__Numbers__NatInt__NZPow.dk.gz
diff --git a/out/Coq__Numbers__NatInt__NZProperties.dk.gz b/out/Coq__Numbers__NatInt__NZProperties.dk.gz
diff --git a/out/Coq__Numbers__NatInt__NZSqrt.dk.gz b/out/Coq__Numbers__NatInt__NZSqrt.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NAdd.dk.gz b/out/Coq__Numbers__Natural__Abstract__NAdd.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NAddOrder.dk.gz b/out/Coq__Numbers__Natural__Abstract__NAddOrder.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NAxioms.dk.gz b/out/Coq__Numbers__Natural__Abstract__NAxioms.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NBase.dk.gz b/out/Coq__Numbers__Natural__Abstract__NBase.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NBits.dk.gz b/out/Coq__Numbers__Natural__Abstract__NBits.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NDiv.dk.gz b/out/Coq__Numbers__Natural__Abstract__NDiv.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NGcd.dk.gz b/out/Coq__Numbers__Natural__Abstract__NGcd.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NLcm.dk.gz b/out/Coq__Numbers__Natural__Abstract__NLcm.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NLog.dk.gz b/out/Coq__Numbers__Natural__Abstract__NLog.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NMaxMin.dk.gz b/out/Coq__Numbers__Natural__Abstract__NMaxMin.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NMulOrder.dk.gz b/out/Coq__Numbers__Natural__Abstract__NMulOrder.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NOrder.dk.gz b/out/Coq__Numbers__Natural__Abstract__NOrder.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NParity.dk.gz b/out/Coq__Numbers__Natural__Abstract__NParity.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NPow.dk.gz b/out/Coq__Numbers__Natural__Abstract__NPow.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NProperties.dk.gz b/out/Coq__Numbers__Natural__Abstract__NProperties.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NSqrt.dk.gz b/out/Coq__Numbers__Natural__Abstract__NSqrt.dk.gz
diff --git a/out/Coq__Numbers__Natural__Abstract__NSub.dk.gz b/out/Coq__Numbers__Natural__Abstract__NSub.dk.gz
diff --git a/out/Coq__Numbers__NumPrelude.dk.gz b/out/Coq__Numbers__NumPrelude.dk.gz
diff --git a/out/Coq__Program__Basics.dk.gz b/out/Coq__Program__Basics.dk.gz
diff --git a/out/Coq__Program__Tactics.dk.gz b/out/Coq__Program__Tactics.dk.gz
diff --git a/out/Coq__Relations__Operators__Properties.dk.gz b/out/Coq__Relations__Operators__Properties.dk.gz
diff --git a/out/Coq__Relations__Relation__Definitions.dk.gz b/out/Coq__Relations__Relation__Definitions.dk.gz
diff --git a/out/Coq__Relations__Relation__Operators.dk.gz b/out/Coq__Relations__Relation__Operators.dk.gz
diff --git a/out/Coq__Relations__Relations.dk.gz b/out/Coq__Relations__Relations.dk.gz
diff --git a/out/Coq__Setoids__Setoid.dk.gz b/out/Coq__Setoids__Setoid.dk.gz
diff --git a/out/Coq__Structures__Equalities.dk.gz b/out/Coq__Structures__Equalities.dk.gz
diff --git a/out/Coq__Structures__GenericMinMax.dk.gz b/out/Coq__Structures__GenericMinMax.dk.gz
diff --git a/out/Coq__Structures__Orders.dk.gz b/out/Coq__Structures__Orders.dk.gz
diff --git a/out/Coq__Structures__OrdersFacts.dk.gz b/out/Coq__Structures__OrdersFacts.dk.gz
diff --git a/out/Coq__Structures__OrdersTac.dk.gz b/out/Coq__Structures__OrdersTac.dk.gz
diff --git a/out/add_requires.sh b/out/add_requires.sh
@@ -0,0 +1,3 @@
+#!/bin/bash
+
+dk dep $@ | cut -d ":" -f 2 | sed "s/ /\n/g" | grep ".dko$" | sed "s/\(.*\)\.dko$/require coq.\\1 as \\1;/g"
diff --git a/out/compile.sh b/out/compile.sh
@@ -0,0 +1,22 @@
+#!/bin/sh
+#set -e
+#set -x
+
+#export PATH=$PWD/_build/install/default/bin:$PATH
+
+for i in *.dk.gz; do rm -f `basename $i .gz`; gunzip -k $i; done
+touch cupicef.dk
+
+for i in *.dk; do
+  LPFILE=`basename $i .dk`.lp
+  # add the flags
+  cat header > $LPFILE
+  # add the exports
+  ./add_requires.sh $i >> $LPFILE
+  lambdapi export -o lp $i >> $LPFILE ;
+done
+cp cupicef.lp.handmade cupicef.lp
+
+rm *.dk
+
+lambdapi check -c Coq__Init__Peano.lp
diff --git a/out/cupicef.lp.handmade b/out/cupicef.lp.handmade
diff --git a/out/header b/out/header
@@ -0,0 +1 @@
+flag "eta_equality" on;
diff --git a/out/lambdapi.pkg b/out/lambdapi.pkg
@@ -0,0 +1,2 @@
+package_name=coq
+root_path=coq
diff --git a/out/test.lp b/out/test.lp
@@ -0,0 +1,53 @@
+require coq.cupicef as bios;
+require coq.Coq__Relations__Relation__Definitions;
+require coq.Coq__Classes__RelationClasses as x;
+require coq.Coq__Init__Logic as y;
+
+open "tc" coq.Coq__Classes__RelationClasses;
+
+flag "print_implicits" on; // default is off
+flag "print_contexts" on; // default is off
+flag "print_domains" on; // default is off
+flag "print_meta_types" on; // default is 
+
+type y.eq;
+type x.reflexivity;
+
+// ENRICO: bug in readback of terms in the query,the context is empty 
+// We hack it with a section variable
+symbol A : bios.Univ (bios.type (bios.s bios.z));
+
+// cast from Type[1] to Type[2]
+coerce_rule coerce (bios.Univ (bios.{|type|} (bios.s bios.z))) (bios.Univ (bios.{|type|} (bios.s (bios.s bios.z)))) $X ↪ (bios.cast (bios.axiom (bios.{|type|} (bios.s bios.z)))
+ (bios.axiom (bios.{|type|} (bios.s (bios.s bios.z))))
+ (bios.univ (bios.{|type|} (bios.s bios.z))
+  (bios.axiom (bios.{|type|} (bios.s bios.z))) bios.I)
+ (bios.univ (bios.{|type|} (bios.s (bios.s bios.z)))
+  (bios.axiom (bios.{|type|} (bios.s (bios.s bios.z)))) bios.I)
+ bios.I
+ $X);
+
+//debug +i;
+//debug +e;
+//debug +u;
+
+type x.reflexivity A (y.eq A) _ _;
+type x.match____RewriteRelation _ A (y.eq A) _ _ _;
+
+/*
+type
+x.reflexivity A (y.eq
+(
+
+bios.cast
+(bios.axiom (bios.{|type|} (bios.s bios.z)))
+(bios.axiom (bios.{|type|} (bios.s (bios.s bios.z))))
+(bios.univ (bios.{|type|} (bios.s bios.z))
+ (bios.axiom (bios.{|type|} (bios.s bios.z))) bios.I)
+(bios.univ (bios.{|type|} (bios.s (bios.s bios.z)))
+ (bios.axiom (bios.{|type|} (bios.s (bios.s bios.z))))
+ bios.I)
+_
+
+A)) _ _;
+*/
diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
@@ -23,6 +23,7 @@ let check_cmd : Config.t -> int option -> string list -> unit =
   let run _ =
     let open Timed in
     Config.init cfg;
+    Elpi_handle.init ();
     (* We save time to run each file in the same environment. *)
     let time = Time.save () in
     let handle file =

diff --git a/src/common/error.ml b/src/common/error.ml
@@ -73,4 +73,6 @@ let handle_exceptions : (unit -> unit) -> unit = fun f ->
   try f () with
   | Fatal(None,    msg) -> exit_with "%s" msg
   | Fatal(Some(p), msg) -> exit_with "[%a] %s" Pos.pp p msg
+  (*
   | e                   -> exit_with "Uncaught [%s]." (Printexc.to_string e)
+  *)
diff --git a/src/core/ctxt.ml b/src/core/ctxt.ml
@@ -4,10 +4,22 @@ open Term
 open Lplib
 open Timed
 
+(** [unbind ctx a def b] returns a triple [(x,t,new_ctx)] such that [(x,t)] is
+    an unbinding of [b] (in the sense of [Bindlib.unbind]) and [new_ctx] is an
+    extension of context [ctx] with the assumption that [x] has type [a] (only
+    if [x] occurs in [t], or [~keep:true]).
+    If [def] is of the form [Some(u)], the context also
+    registers the term [u] as the definition of variable [x]. *)
+let unbind : ?keep:bool -> 'a actxt -> 'a -> term option -> tbinder ->
+  tvar * term * 'a actxt =
+  fun ?(keep=false) ctx a def b ->
+  let (x, t) = Bindlib.unbind b in
+  (x, t, if keep || Bindlib.binder_occur b then (x, a, def) :: ctx else ctx)
+
 (** [type_of x ctx] returns the type of [x] in the context [ctx] when it
     appears in it, and
 @raise [Not_found] otherwise. *)
-let type_of : tvar -> ctxt -> term = fun x ctx ->
+let type_of : tvar -> 'a actxt -> 'a = fun x ctx ->
   let (_,a,_) = List.find (fun (y,_,_) -> Bindlib.eq_vars x y) ctx in a
 
 (** [def_of x ctx] returns the definition of [x] in the context [ctx] if it

diff --git a/src/core/dune b/src/core/dune
@@ -10,4 +10,4 @@
  (public_name lambdapi.core)
  (synopsis "LambdaPi interactive theorem prover [core]")
  (modules :standard)
- (libraries lambdapi.common lambdapi.lplib pratter bindlib why3))
+ (libraries lambdapi.common lambdapi.lplib pratter bindlib why3 elpi))
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		#!/bin/bash

		dk dep $@ \| cut -d ":" -f 2 \| sed "s/ /\n/g" \| grep ".dko$" \| sed "s/\(.*\)\.dko$/require coq.\\1 as \\1;/g"