Merge pull request #114 from LPCIC/cleanup

Cleanup before tackling tabling

Author: gares

CHANGES.md

@@ -3,6 +3,8 @@
 - Runtime/FFI:
   - fix handling of eta expanded unification variables. Many thanks to
     Nathan Guermond for testing this tricky case.
+  - Change `Rawdata.Constants.eqc` to a builtin
+  - Fix `Rawdata.Constants.cutc` has always been a builtin
 
 # v1.13.7 (July 2021)
 

elpi_REPL.ml

@@ -61,7 +61,8 @@ let usage =
   "\t-no-tc don't typecheck the program\n" ^ 
   "\t-delay-problems-outside-pattern-fragment (deprecated, for Teyjus\n" ^
   "\t                                          compatibility)\n" ^
-  "\t-version prints the version of Elpi\n" ^ 
+  "\t--version prints the version of Elpi (also -v or -version)\n" ^ 
+  "\t--help prints this help (also -h or -help)\n" ^ 
  API.Setup.usage ^
   "\nDebug options (for debugging Elpi, not your program):\n" ^ 
   "\t-print-accumulated-files prints files loaded via accumulate\n" ^ 
@@ -103,8 +104,8 @@ let _ =
     | "-no-tc" :: rest -> typecheck := false; eat_options rest
     | "-document-builtins" :: rest -> doc_builtins := true; eat_options rest
     | "-D" :: var :: rest -> vars := API.Compile.StrSet.add var !vars; eat_options rest
-    | ("-h" | "--help") :: _ -> Printf.eprintf "%s" usage; exit 0
-    | "-version" :: _ -> Printf.printf "%s\n" "%%VERSION_NUM%%"; exit 0
+    | ("-h" | "--help" | "-help") :: _ -> Printf.eprintf "%s" usage; exit 0
+    | ("-v" | "--version" | "-version") :: _ -> Printf.printf "%s\n" "%%VERSION_NUM%%"; exit 0
     | "--" :: rest -> rest
     | x :: rest -> x :: eat_options rest
   in

src/API.ml

@@ -176,7 +176,7 @@ end
 module Pp = struct
   let term pp_ctx f t = (* XXX query depth *)
     let module R = (val !r) in let open R in
-    R.Pp.uppterm ~pp_ctx 0 [] 0 [||] f t
+    R.Pp.uppterm ~pp_ctx 0 [] ~argsdepth:0 [||] f t
 
   let constraints pp_ctx f c =
     let module R = (val !r) in let open R in
@@ -186,7 +186,7 @@ module Pp = struct
 
   let query f c =
     let module R = (val !r) in let open R in
-    Compiler.pp_query (fun ~pp_ctx ~depth -> R.Pp.uppterm ~pp_ctx depth [] 0 [||]) f c
+    Compiler.pp_query (fun ~pp_ctx ~depth -> R.Pp.uppterm ~pp_ctx depth [] ~argsdepth:0 [||]) f c
 
   module Ast = struct
     let program = EA.Program.pp

src/API.mli

@@ -954,14 +954,14 @@ module RawData : sig
 
     val show : constant -> string
 
-    val eqc    : constant (* = *)
+    val eqc    : builtin (* = *)
     val orc    : constant (* ; *)
     val andc   : constant (* , *)
     val rimplc : constant (* :- *)
     val pic    : constant (* pi *)
     val sigmac : constant (* sigma *)
     val implc  : constant (* => *)
-    val cutc   : constant (* ! *)
+    val cutc   : builtin (* ! *)
 
     (* LambdaProlog built-in data types are just instances of CData.
      * The typeabbrev machinery translates [int], [float] and [string]

src/builtin.elpi

@@ -12,9 +12,7 @@ pred fail.
 
 pred false.
 
-pred (=) o:A, o:A.
-
-X = X.
+external pred (=) o:A, o:A. % unification
 
 typeabbrev int (ctype "int").
 
@@ -512,7 +510,7 @@ external pred random.int i:int, o:int.
 % Conventions:
 % - all predicates declare a mode with some input arguments, unless...
 % - predicates whose name ends with R are relations (work in any direction,
-%   that is all arguments are in ouput mode)
+%   that is all arguments are in output mode)
 % - predicates whose name ends with ! do contain a cut and generate only the
 %   first result
 % - all errors given by this library end up calling fatal-error[-w-data],

src/builtin.ml

@@ -395,9 +395,8 @@ let core_builtins = let open BuiltIn in let open ContextualConversion in [
   LPCode "pred fail.";
   LPCode "pred false.";
 
-  LPCode "pred (=) o:A, o:A.";
-  LPCode "X = X.";
-
+  LPCode "external pred (=) o:A, o:A. % unification";
+  
   MLData BuiltInData.int;
   MLData BuiltInData.string;
   MLData BuiltInData.float;

src/builtin_stdlib.elpi

@@ -3,7 +3,7 @@
 % Conventions:
 % - all predicates declare a mode with some input arguments, unless...
 % - predicates whose name ends with R are relations (work in any direction,
-%   that is all arguments are in ouput mode)
+%   that is all arguments are in output mode)
 % - predicates whose name ends with ! do contain a cut and generate only the
 %   first result
 % - all errors given by this library end up calling fatal-error[-w-data],

src/compiler.ml

@@ -312,6 +312,7 @@ let is_declared_str state x =
   || x == Symbols.(show state D.Global_symbols.declare_constraintc)
   || x == Symbols.(show state D.Global_symbols.print_constraintsc)
   || x == Symbols.(show state D.Global_symbols.cutc)
+  || x == Symbols.(show state D.Global_symbols.eqc)
   || x == Symbols.(show state D.Global_symbols.findall_solutionsc)
 ;;
 
@@ -321,6 +322,7 @@ let is_declared state x =
   || x == D.Global_symbols.declare_constraintc
   || x == D.Global_symbols.print_constraintsc
   || x == D.Global_symbols.cutc
+  || x == D.Global_symbols.eqc
   || x == D.Global_symbols.findall_solutionsc
 ;;
 
@@ -2128,7 +2130,7 @@ let query_of_ast (compiler_state, assembled_program) t =
   let query_env = Array.make query.amap.nargs D.dummy in
   let state, queryt = stack_term_of_preterm ~depth:initial_depth state query in
   let initial_goal =
-    R.move ~adepth:initial_depth ~from:initial_depth ~to_:initial_depth query_env
+    R.move ~argsdepth:initial_depth ~from:initial_depth ~to_:initial_depth query_env
       queryt in
   let assignments = StrMap.map (fun i -> query_env.(i)) query.amap.n2i in
   {
@@ -2159,7 +2161,7 @@ let query_of_term (compiler_state, assembled_program) f =
   let query_env = Array.make query.amap.nargs D.dummy in
     let state, queryt = stack_term_of_preterm ~depth:initial_depth state query in
   let initial_goal =
-    R.move ~adepth:initial_depth ~from:initial_depth ~to_:initial_depth query_env
+    R.move ~argsdepth:initial_depth ~from:initial_depth ~to_:initial_depth query_env
       queryt in
   let assignments = StrMap.map (fun i -> query_env.(i)) query.amap.n2i in
  {
@@ -2533,7 +2535,7 @@ let term_of_ast ~depth state t =
     ) state t in
  let env = Array.make nargs D.dummy in
  let argsdepth = depth in
- state, R.move ~adepth:argsdepth ~from:depth ~to_:depth env t
+ state, R.move ~argsdepth ~from:depth ~to_:depth env t
 ;;
 
 let static_check ~exec ~checker:(state,program)