wip

Makefile

@@ -26,6 +26,7 @@ bnf:
 
 .PHONY: tests
 tests: lambdapi
+	@dune exec --only-packages lambdapi -- tests/export_raw_dk.sh
 	@dune runtest
 	@dune exec --only-packages lambdapi -- tests/runtests.sh
 	@dune exec --only-packages lambdapi -- tests/dtrees.sh
@@ -169,4 +170,3 @@ uninstall_vim_mode:
 .PHONY: build-vscode-extension
 build-vscode-extension:
 	cd editors/vscode && make && mkdir extensionFolder && vsce package -o extensionFolder
-

src/export/rawdk.ml

@@ -1,6 +1,6 @@
 (** Translate the parser-level AST to Dedukti. *)
 
-open Lplib open Base
+open Lplib open Base open Extra
 open Common open Pos open Error
 open Parsing open Syntax
 open Format
@@ -19,11 +19,11 @@ let raw_path : Path.t pp = List.pp string "."
 
 let path : p_path pp = fun ppf {elt;_} -> raw_path ppf elt
 
-let qident : p_qident pp = fun ppf {elt=(mp,s);pos} ->
+let qident : p_qident pp = fun ppf ({elt=(mp,s);pos} as qid) ->
   match mp with
   | [] -> raw_ident ppf s
   | [_;m] -> out ppf "%a.%a" raw_ident m raw_ident s
-  | _ -> fatal pos "Cannot be translated."
+  | _ -> fatal pos "Cannot be translated: %a.@." Pretty.qident qid
 
 let rec term : p_term pp = fun ppf t ->
   match t.elt with
@@ -79,7 +79,7 @@ let strat : Eval.strat pp = fun ppf {strategy; steps} ->
   | SNF, None -> ()
   | SNF, Some k -> out ppf "[%d]" k
 
-let query : p_query pp = fun ppf {elt;pos} ->
+let query : p_query pp = fun ppf ({elt;pos} as q) ->
   match elt with
   | P_query_verbose _
   | P_query_debug _
@@ -88,56 +88,75 @@ let query : p_query pp = fun ppf {elt;pos} ->
   | P_query_print _
   | P_query_proofterm
   | P_query_search _
-  | P_query_flag _
+  | P_query_flag _ -> out ppf "(;%a;)" Pretty.query q (*FIXME?*)
   | P_query_infer(_,{strategy=(SNF|HNF|WHNF);_})
   | P_query_normalize(_,{strategy=(NONE|HNF);_}) ->
-      fatal pos "Cannot be translated."
+      fatal pos "Cannot be translated: %a" Pretty.query q
   | P_query_assert(b,a) -> assertion ppf (b,a)
   | P_query_infer(t,{strategy=NONE;_}) -> out ppf "#INFER %a.@." term t
   | P_query_normalize(t,s) -> out ppf "#EVAL%a %a.@." strat s term t
 
-let modifier : p_modifier pp = fun ppf {elt;pos} ->
+let modifier : bool -> p_modifier pp = fun ac ppf ({elt;pos} as m) ->
   match elt with
   | P_mstrat Eager
   | P_expo Public
   | P_prop Const -> ()
   | P_expo Protec -> out ppf "private "
-  | P_prop Defin -> out ppf "def "
+  | P_prop Defin -> if ac then out ppf "defac " else out ppf "def "
   | P_prop Injec -> out ppf "injective "
-  | P_prop (AC _) -> out ppf "AC "
   | P_opaq -> out ppf "thm "
-  | P_mstrat Sequen
-  | P_expo Privat
-  | P_prop Commu
-  | P_prop (Assoc _) -> fatal pos "Cannot be translated."
-
-let rule : p_rule pp = fun ppf {elt=(l,r);_} ->
-  let vars = [] in
-  out ppf "[%a] %a --> %a.@." (List.pp ident " ") vars term l term r
-
-let command : p_command pp = fun ppf {elt; pos} ->
+  | P_expo Privat -> out ppf "(;private;) " (*FIXME?*)
+  | P_mstrat Sequen ->
+      fatal pos "Cannot be translated: %a@." Pretty.modifier m
+  | P_prop (AC _) -> assert false
+  | P_prop Commu -> assert false
+  | P_prop (Assoc _) -> assert false
+
+let a_or_c {elt;_} =
+  match elt with
+  | P_prop (AC _) -> assert false
+  | P_prop Commu | P_prop (Assoc _) -> true
+  | _ -> false
+
+let is_ac ms =
+  match ms with
+  | [] -> false
+  | [{elt=P_prop Commu;_}; {elt=P_prop(Assoc _);_}]
+  | [{elt=P_prop(Assoc _);_}; {elt=P_prop Commu;_}] -> true
+  | [{elt=P_prop Commu;pos} as m]
+  | [{elt=P_prop(Assoc _);pos} as m] ->
+      fatal pos "Cannot be translated: %a@." Pretty.modifier m
+  | {pos;_}::_ -> fatal pos "Modifier repetition."
+
+let rule : p_rule pp =
+  let varset ppf set = List.pp string " " ppf (StrSet.elements set) in
+  fun ppf {elt=(l,r);_} ->
+  out ppf "[%a] %a --> %a.@." varset (pvars_lhs l) term l term r
+
+let command : p_command pp = fun ppf ({elt; pos} as c) ->
   match elt with
   | P_query q -> query ppf q
   | P_require(false,ps) -> out ppf "#REQUIRE %a.@." (List.pp path " ") ps
-  | P_symbol{p_sym_mod; p_sym_nam=n; p_sym_arg=xs; p_sym_typ=Some a;
+  | P_symbol{p_sym_mod; p_sym_nam=n; p_sym_arg=xs; p_sym_typ;
              p_sym_trm; p_sym_prf=None; p_sym_def=_;} ->
-      let dfn ppf = out ppf " := %a%a.@." abs xs term in
-      out ppf "%a%a : %a%a%a.@."
-        (List.pp modifier "") p_sym_mod ident n prod xs term a
-        (Option.pp dfn) p_sym_trm
-  | P_rules _ -> assert false (*TODO*)
+      let typ ppf = out ppf " : %a%a" prod xs term in
+      let dfn ppf = out ppf " := %a%a" abs xs term in
+      let ac, ms = List.partition a_or_c p_sym_mod in
+      out ppf "%a%a%a%a.@." (List.pp (modifier (is_ac ac)) "") ms ident n
+        (Option.pp typ) p_sym_typ (Option.pp dfn) p_sym_trm
+  | P_rules rs -> List.iter (rule ppf) rs
+  | P_builtin _
+  | P_unif_rule _
+  | P_coercion _
+    -> () (*FIXME?*)
   | P_inductive _
   | P_open _
   | P_require_as _
-  | P_builtin _
   | P_notation _
-  | P_unif_rule _
-  | P_coercion _
   | P_opaque _
   | P_require(true,_)
-  | P_symbol{p_sym_typ=None; p_sym_prf=None; _}
   | P_symbol{p_sym_prf=Some _; _}
-    -> fatal pos "Cannot be translated."
+    -> fatal pos "Cannot be translated: %a" Pretty.command c
 
 let ast : ast pp = fun ppf -> Stream.iter (command ppf)
 

src/parsing/syntax.ml

@@ -107,6 +107,30 @@ let p_get_args : p_term -> p_term * p_term list = fun t ->
     | _            -> t, acc
   in p_get_args t []
 
+(** [pvars_lhs t] computes the set of pattern variable names in [t], assuming
+    that [t] is a rule LHS. *)
+let rec pvars_lhs : p_term -> StrSet.t = fun {elt;pos} ->
+  match elt with
+  | P_Type
+  | P_Iden _
+  | P_Wild
+  | P_Patt(None,_)
+  | P_NLit _
+    -> StrSet.empty
+  | P_Meta _
+  | P_LLet _
+  | P_Arro _
+  | P_Prod _
+    -> assert false
+  | P_Patt(Some{elt;_},_) ->
+      StrSet.singleton elt
+  | P_Appl(u,v) ->
+      StrSet.union (pvars_lhs u) (pvars_lhs v)
+  | P_Abst(_,u)
+  | P_Wrap u
+  | P_Expl u
+    -> pvars_lhs u
+
 (** Parser-level rewriting rule representation. *)
 type p_rule_aux = p_term * p_term
 type p_rule = p_rule_aux loc

tests/export_raw_dk.sh

@@ -0,0 +1,87 @@
+#!/bin/bash
+
+echo '############ test export -o raw_dk ############'
+
+lambdapi=${LAMBDAPI:-_build/install/default/bin/lambdapi}
+dkcheck=${DKCHECK:-dk check}
+dkdep=${DKDEP:-dk dep}
+
+TIMEFORMAT="%Es"
+
+root=`pwd`
+
+outdir=/tmp/export_raw_dk
+
+reset_outdir() {
+    rm -rf $outdir
+    mkdir -p $outdir
+}
+reset_outdir
+
+# compute lp files to test
+cd tests/OK
+for f in *.lp
+do
+    f=${f%.lp}
+    case $f in
+        ac);; # because dedukti does not handle commutative and non associative symbols
+        π/utf_path);; # because dedukti does not accept unicode characters in module names
+        escape_path|'tests/OK/a b/escape file');; # because dedukti does not accept spaces in module names
+        262_private_in_lhs);; # because dedukti does not accept protected symbols in rule LHS arguments
+        273|tests/OK/813);; # because dedukti SR algorithm fails
+        file.with.dot|req.file.with.dot);; #FIXME
+        indind);; #FIXME
+        rule_order);; #because it contains sequential
+        xor|Set|quant*|Prop|prefix|parametricCoercions|opaque|nat_id*|michael|max-suc-alg|lpparse);; #because it contains notation
+        require_nondkmident);; #because it uses a nested module name
+        why3*|tutorial|try|tautologies|rewrite*|remove|natproofs);; #because it contains proofs
+        triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2);; #because it contains open
+        plus_ac);; #because it contains associative or commutative alone
+        strictly_positive_*);; #because it contains inductive
+        *) lp_files="tests/OK/$f.lp $lp_files";
+           f=`echo $f | sed -e 's/\//_/g'`;
+           dk_files="tests/OK/$f.dk $dk_files";;
+    esac
+done
+cd ../..
+
+# compile lp files
+compile() {
+    echo 'compile lp files ...'
+    #$lambdapi check -w -c $lp_files # does not work because of #802
+    for f in $lp_files
+    do
+        echo "compile $f ..."
+        $lambdapi check -w -v 0 -c $f
+    done
+}
+#time compile
+
+# translate lp files to dk files
+translate() {
+    echo 'translate lp files ...'
+    for f in $lp_files
+    do
+        f=${f%.lp}
+        out=$outdir/`echo $f | sed -e 's/\//_/g'`
+        echo "$f.lp --> $out.dk ..."
+        $lambdapi export -w -v 0 -o raw_dk $f.lp > $out.dk
+        if test $? -ne 0; then echo KO; exit 1; fi
+    done
+}
+time translate
+
+# check dk files
+check() {
+    cd $outdir
+    echo 'remove #REQUIRE commands (to be removed when https://github.com/Deducteam/Dedukti/issues/262 is fixed) ...'
+    sed -i -e 's/#REQUIRE.*$//' $dk_files
+    dk_files=`$dkdep -q -s $dk_files`
+    echo $dkcheck -q -e $dk_files ...
+    $dkcheck -q -e $dk_files
+    res=$?
+    cd $root
+    if test $res -ne 0; then echo KO; else echo OK; fi
+    exit $res
+}
+time check