wip

src/common/escape.ml

@@ -1,4 +1,5 @@
 (** Escaped identifiers ["{|...|}"]. *)
+let escape : string -> string = fun s -> "{|" ^ s ^ "|}"
 
 (** [is_escaped s] tells if [s] begins with ["{|"] and ends with ["|}"]
    without overlapping. For efficiency, we just test that it starts with
@@ -13,10 +14,10 @@ let unescape : string -> string = fun s ->
    too, then [add_prefix p n] is just [p ^ n]. Otherwise, it is ["{|" ^ p ^
    unescape n ^ "|}"]. *)
 let add_prefix : string -> string -> string = fun p n ->
-  if is_escaped n then "{|" ^ p ^ unescape n ^ "|}" else p ^ n
+  if is_escaped n then escape (p ^ unescape n) else p ^ n
 
 (** [s] is assumed to be a regular identifier. If [n] is a regular identifier
    too, then [add_suffix n s] is just [n ^ s]. Otherwise, it is ["{" ^
    unescape n ^ s ^ "|}"]. *)
 let add_suffix : string -> string -> string = fun n s ->
-  if is_escaped n then "{|" ^ unescape n ^ s ^ "|}"  else n ^ s
+  if is_escaped n then escape (unescape n ^ s)  else n ^ s

src/export/dk.ml

@@ -56,33 +56,30 @@ let is_ident : string -> bool = fun s ->
 let is_mident : string -> bool = fun s ->
   Parsing.DkLexer.is_mident (Lexing.from_string s)
 
-let escape : string pp = fun ppf s -> out ppf "{|%s|}" s
-
-let replace_spaces : string -> string = fun s ->
+(*let replace_spaces : string -> string = fun s ->
   let open Bytes in
   let b = of_string s in
   for i=0 to length b - 1 do
     match get b i with
     | ' ' | '\n' -> set b i '_'
     | _ -> ()
   done;
-  to_string b
+  to_string b*)
 
 let ident : string pp = fun ppf s ->
-  if s = "" then escape ppf s
-  else if s.[0] = '{' then string ppf (replace_spaces s)
-  else if is_keyword s then escape ppf s
-  else if is_ident s then string ppf s
-  else escape ppf s
+  string ppf
+    (if s = "" then Escape.escape s
+     else if s.[0] = '{' then s
+     else if is_keyword s then Escape.escape s
+     else if is_ident s then s
+     else Escape.escape s)
 
 (** Translation of paths. Paths equal to the [!current_path] are not
    printed. Non-empty paths end with a dot. We assume that the module p1.p2.p3
    is in the file p1_p2_p3.dk. *)
 
 let path_elt : string pp = fun ppf s ->
-  if s <> "" && s.[0] = '{' then
-    string ppf (replace_spaces (Escape.unescape s))
-  else string ppf s
+  string ppf (if Escape.is_escaped s then Escape.unescape s else s)
 
 let current_path = Stdlib.ref []
 
@@ -91,11 +88,9 @@ let path : Path.t pp = fun ppf p ->
   match p with
   | [] -> ()
   | p ->
-      let joined_path = Format.asprintf "%a" (List.pp path_elt "_") p in
-      if List.for_all is_mident p then
-        out ppf "%s." joined_path
-      else
-        Format.fprintf ppf "%a." escape joined_path
+      let m = Format.asprintf "%a" (List.pp path_elt "_") p in
+      let m = if is_mident m then m else Escape.escape m in
+      out ppf "%s." m
 
 let qid : (Path.t * string) pp = fun ppf (p, i) ->
   out ppf "%a%a" path p ident i

src/export/rawdk.ml

@@ -4,9 +4,9 @@ open Lplib open Base open Extra
 open Common open Pos open Error
 open Parsing open Syntax
 open Format
-open Core open Eval
+open Core open Eval open Term
 
-let raw_ident : string pp = string
+let raw_ident : string pp = fun ppf s -> Dk.ident ppf s
 
 let ident : p_ident pp = fun ppf {elt;_} -> raw_ident ppf elt
 
@@ -34,41 +34,80 @@ let rec term : p_term pp = fun ppf t ->
   | P_Wild -> out ppf "_"
   | P_NLit i -> string ppf i
   | P_Iden(qid,_) -> qident ppf qid
-  | P_Arro(u,v) -> out ppf "(%a -> %a)" term u term v
-  | P_Abst(xs,u) -> out ppf "(%a%a)" abs xs term u
-  | P_Prod(xs,u) -> out ppf "(%a%a)" prod xs term u
-  | P_LLet(x,xs,None,u,v) ->
-      out ppf "((%a => %a) (%a%a))" ident x term v abs xs term u
-  | P_LLet(x,xs,Some a,u,v) ->
-      out ppf "((%a : %a%a => %a) (%a%a))"
-        ident x prod xs term a term v abs xs term u
+  | P_Arro(u,v) -> out ppf "%a -> %a" pterm u term v
+  | P_Abst(xs,u) -> out ppf "%a%a" abs xs term u
+  | P_Prod(xs,u) -> out ppf "%a%a" prod xs term u
+  | P_LLet(x,xs,a,u,v) ->
+      out ppf "(%a%a => %a) %a"
+        ident x (Option.pp (let_typ xs)) a term v (let_dfn xs) u
   | P_Wrap u -> out ppf "(%a)" term u
-  | P_Appl(u,v) -> out ppf "(%a %a)" term u term v
+  | P_Appl(u,v) -> out ppf "%a %a" term u pterm v
+
+and let_typ : p_params list -> p_term pp = fun xs ppf u ->
+  match xs with
+  | [] -> typ ppf u
+  | _ -> out ppf ": (%a%a)" prod xs term u
+
+and let_dfn : p_params list -> p_term pp = fun xs ppf u ->
+  match xs with
+  | [] -> pterm ppf u
+  | _ -> out ppf "(%a%a)" abs xs term u
+
+and pterm : p_term pp = fun ppf t ->
+  match t.elt with
+  (* doesn't need surrounding parentheses *)
+  | P_Meta _
+  | P_Patt(_,None)
+  | P_Expl _
+  | P_Type
+  | P_Wild
+  | P_NLit _
+  | P_Iden _
+  | P_Wrap _
+    -> term ppf t
+  (* add surrounding parentheses *)
+  | P_Patt(_,Some _)
+  | P_Arro _
+  | P_Abst _
+  | P_Prod _
+  | P_LLet _
+  | P_Appl _
+    -> out ppf "(%a)" term t
 
 and terms : p_term array pp = fun ppf -> Array.iter (out ppf " %a" term)
 
-and param : p_term option -> string -> p_ident option pp =
-  fun a sep ppf id -> out ppf "%a%a%s" param_id id typopt a sep
+and param : p_term option -> string -> p_ident option pp = fun a sep ppf id ->
+  if sep = "" then
+    match a with
+    | None -> out ppf " %a" param_id id
+    | Some a -> out ppf " (%a%a)" param_id id typ a
+  else out ppf "%a%a%s" param_id id (Option.pp typ) a sep
 
 and params : string -> p_params pp = fun sep ppf (ids,a,_) ->
-  List.iter (out ppf "%a" (param a sep)) ids
+  match ids, a with
+  | None::_, None ->
+      fatal_no_pos "Cannot translate \"_\" parameters with no type."
+  | Some {pos;_}::_, None ->
+      fatal pos "Cannot translate parameters with no type."
+  | _ -> List.iter (out ppf "%a" (param a sep)) ids
 
 and params_list : string -> p_params list pp = fun sep ppf ->
   List.iter (out ppf "%a" (params sep))
 
 and abs : p_params list pp = fun ppf -> params_list " => " ppf
-
 and prod : p_params list pp = fun ppf -> params_list " -> " ppf
+and arg : p_params list pp = fun ppf -> params_list "" ppf
 
-and typopt : p_term option pp = fun ppf t ->
-  Option.iter (out ppf " : %a" term) t
+and typ : p_term pp = fun ppf t -> out ppf " : %a" pterm t
 
 let bool : bool pp = fun ppf b -> if not b then out ppf "NOT"
 
 let assertion : (bool * p_assertion) pp = fun ppf (b,a) ->
   match a with
-  | P_assert_typing(t,u) -> out ppf "#ASSERT%a %a : %a.@." bool b term t term u
-  | P_assert_conv(t,u) -> out ppf "#ASSERT%a %a == %a.@." bool b term t term u
+  | P_assert_typing(t,u) ->
+      out ppf "#ASSERT%a %a : %a.@." bool b term t term u
+  | P_assert_conv(t,u) ->
+      out ppf "#ASSERT%a %a == %a.@." bool b pterm t pterm u
 
 let strat : Eval.strat pp = fun ppf {strategy; steps} ->
   match strategy, steps with
@@ -92,58 +131,83 @@ let query : p_query pp = fun ppf ({elt;pos} as q) ->
   | P_query_infer(_,{strategy=(SNF|HNF|WHNF);_})
   | P_query_normalize(_,{strategy=(NONE|HNF);_}) ->
       fatal pos "Cannot be translated: %a" Pretty.query q
-  | P_query_assert(b,a) -> assertion ppf (b,a)
+  | P_query_assert(b,a) -> assertion ppf (not 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 : 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 -> if ac then out ppf "defac " else out ppf "def "
-  | P_prop Injec -> out ppf "injective "
-  | P_opaq -> out ppf "thm "
-  | 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;_} =
+(*https://github.com/Deducteam/Dedukti/issues/318*)
+let rec remove_wraps ({elt;_} as t) =
   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."
+  | P_Wrap u -> remove_wraps u
+  | _ -> t
 
 let rule : p_rule pp =
-  let varset ppf set = List.pp string " " ppf (StrSet.elements set) in
+  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
+  out ppf "[%a] %a --> %a.@." varset (pvars_lhs l) term (remove_wraps l) term r
+
+let partition_modifiers ms =
+  let ms = List.map (fun {elt;_} -> elt) ms in
+  let ms = List.sort_uniq Stdlib.compare ms in
+  let is_prop elt = match elt with P_prop _ -> true | _ -> false in
+  let props, non_props = List.partition is_prop ms in
+  let props = List.map (function P_prop p -> p | _ -> assert false) props in
+  let is_expo elt = match elt with P_expo _ -> true | _ -> false in
+  let expos, non_expos = List.partition is_expo non_props in
+  let expos = List.map (function P_expo e -> e | _ -> assert false) expos in
+  let is_mstrat elt = match elt with P_mstrat _ -> true | _ -> false in
+  let mstrats, opaqs = List.partition is_mstrat non_expos in
+  let mstrats =
+    List.map (function P_mstrat s -> s | _ -> assert false) mstrats in
+  (* we ignore private symbols *)
+  let expos = List.filter (function Privat -> false | _ -> true) expos in
+  props, expos, mstrats, opaqs
+
+(* check Stdlib.compare on modifiers. *)
+let _ =
+  assert (Stdlib.compare Commu (Assoc true) < 0)
+  ;assert (Stdlib.compare Commu (Assoc false) < 0)
+
+(* translation of lists of modifiers:
+- [opaque] --> "thm"
+- [protected?; associative; commutative] --> "private"? "defac"
+- [protected?; injective] --> "private"? "injective"
+- [protected] --> "private"
+- [constant] --> ""
+- [] --> "def" *)
+let modifiers : p_term option -> p_modifier list pp = fun p_sym_typ ppf ms ->
+  match partition_modifiers ms with
+  | [], [], [], [] -> out ppf "def "
+  | [], [], [], [P_opaq] when p_sym_typ <> None -> out ppf "thm "
+  (*https://github.com/Deducteam/Dedukti/issues/319*)
+  | [Commu;Assoc _], [Protec], [], [] -> out ppf "defac "
+  | [Injec], [Protec], [], [] -> out ppf "private injective "
+  | [Injec], [], [], [] -> out ppf "injective "
+  | [], [Protec], [], [] -> out ppf "private "
+  | [Const], [], [], [] -> ()
+  | _ ->
+      match ms with
+      | [] -> assert false
+      | {pos;_}::_ -> fatal pos "Cannot translate: %a.@." Pretty.modifiers ms
 
 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_require(false,ps) ->
+      List.iter (fun {elt;_} -> out ppf "#REQUIRE %a@." Dk.path elt) ps
   | 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 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
+      begin match p_sym_trm, p_sym_typ with
+      | Some t, _ ->
+          let dfn ppf = out ppf " := %a" term in
+          out ppf "%a%a%a%a%a.@." (modifiers p_sym_typ) p_sym_mod ident n
+            arg xs (Option.pp typ) p_sym_typ dfn t
+      | None, Some a ->
+          (*https://github.com/Deducteam/Dedukti/issues/322*)
+          out ppf "%a%a : %a%a.@." (modifiers p_sym_typ) p_sym_mod ident n
+            prod xs term a
+      | _ -> assert false
+      end
   | P_rules rs -> List.iter (rule ppf) rs
   | P_builtin _
   | P_unif_rule _
@@ -152,7 +216,7 @@ let command : p_command pp = fun ppf ({elt; pos} as c) ->
   | P_inductive _
   | P_open _
   | P_require_as _
-  | P_notation _
+  | P_notation _ (* FIXME: accept quantifier notations *)
   | P_opaque _
   | P_require(true,_)
   | P_symbol{p_sym_prf=Some _; _}

src/parsing/lpLexer.ml

@@ -173,7 +173,7 @@ let escid = [%sedlex.regexp?
 
 (** [escape s] converts a string [s] into an escaped identifier if it is not
    regular. We do not check whether [s] contains ["|}"]. FIXME? *)
-let escape s = if is_regid s then s else "{|" ^ s ^ "|}"
+let escape s = if is_regid s then s else Escape.escape s
 
 (** [remove_useless_escape s] replaces escaped regular identifiers by their
    unescape form. *)

src/parsing/pretty.ml

@@ -77,8 +77,7 @@ let _ = let open LpLexer in
     ; "with", WITH ]
 
 let raw_ident : string pp = fun ppf s ->
-  if is_keyword s then out ppf "{|%s|}" s
-  else string ppf s
+  string ppf (if is_keyword s then Escape.escape s else s)
 
 let ident : p_ident pp = fun ppf {elt;_} -> raw_ident ppf elt
 

tests/export_dk.sh

@@ -1,5 +1,7 @@
 #!/bin/bash
 
+set -e
+
 echo '############ test export -o dk ############'
 
 lambdapi=${LAMBDAPI:-_build/install/default/bin/lambdapi}
@@ -23,14 +25,20 @@ for f in tests/OK/*.lp
 do
     f=${f%.lp}
     case $f in
-        tests/OK/ac);; # because dedukti does not handle commutative and non associative symbols
-        tests/OK/π/utf_path);; # because dedukti does not accept unicode characters in module names
-        tests/OK/escape_path|'tests/OK/a b/escape file');; # because dedukti does not accept spaces in module names
-        tests/OK/262_private_in_lhs);; # because dedukti does not accept protected symbols in rule LHS arguments
-        tests/OK/273|tests/OK/813);; # because dedukti SR algorithm fails
-        tests/OK/file.with.dot|tests/OK/req.file.with.dot);; #FIXME
-        tests/OK/indind);; #FIXME
-        tests/OK/why3*);; #FIXME
+        # commutative and non associative symbol
+        tests/OK/ac);;
+        # unicode character in module name
+        tests/OK/π/utf_path);;
+        # space in module name
+        tests/OK/escape_path|'tests/OK/a b/escape file');;
+        # protected symbol in rule LHS arguments
+        tests/OK/262_private_in_lhs);;
+        # dedukti SR algorithm fails
+        tests/OK/273|tests/OK/813);;
+        #FIXME
+        tests/OK/file.with.dot|tests/OK/req.file.with.dot);;
+        tests/OK/indind);;
+        tests/OK/why3*);;
         *) lp_files="$f.lp $lp_files";
            f=`echo $f | sed -e 's/\//_/g'`;
            dk_files="$f.dk $dk_files";;
@@ -68,9 +76,17 @@ 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
+    #dk_files=`$dkdep -q -s $dk_files`
+    echo > Makefile <<__END__
+FILES := $(wildcard *.dk)
+default: $(FILES:%.dk=%.dko)
+%.dko: %.dk
+	dk check -e $<
+__END__
+    $dkdep -q $dk_files >> Makefile
+    #echo $dkcheck -q -e $dk_files ...
+    #$dkcheck -q -e $dk_files
+    make
     res=$?
     cd $root
     if test $res -ne 0; then echo KO; else echo OK; fi