wip

Author: gares

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)
+  *)

src/core/elpi_lambdapi.ml

@@ -22,7 +22,8 @@ module Elpi_AUX = struct
     | Some x ->
         let { Common.Pos.fname; start_line; start_col; _ } = x in
         {
-          Ast.Loc.source_name = (match fname with None -> "(.)" | Some x -> x);
+          Ast.Loc.source_name =
+            (match fname with None -> "(.)" | Some x -> x);
           source_start = 0;
           source_stop = 0;
           line = start_line;
@@ -116,7 +117,16 @@ let embed_term : Term.term Conversion.embedding = fun ~depth st t ->
             State.update metamap st (MM.add flex meta), flex in
         let st, args = Elpi_AUX.array_map_fold (aux ~depth ctx) st args in
         st, mkUnifVar flex ~args:(Array.to_list args) st
-    | Plac _ -> Common.Error.fatal_no_pos "embed_term: Plac not implemented"
+    | Plac _ ->
+        let args = List.map (fun (_,x,_) -> mkBound x) ctx in
+        let st, flex = FlexibleData.Elpi.make st in
+        let st, meta = State.update_return pb st (fun pb ->
+          let m1 = LibMeta.fresh pb mk_Type 0 in
+          let m2 = LibMeta.fresh pb (mk_Meta (m1,[||]))
+            (List.length args) in (* empty context is surely wrong *)
+          pb, m2) in
+        let st = State.update metamap st (MM.add flex meta) in
+        st, mkUnifVar flex ~args st
     | Patt _ -> Common.Error.fatal_no_pos "embed_term: Patt not implemented"
     | TEnv _ -> Common.Error.fatal_no_pos "embed_term: TEnv not implemented"
     | Wild   -> Common.Error.fatal_no_pos "embed_term: Wild not implemented"
@@ -167,7 +177,8 @@ fun ~depth st t ->
           with Not_found ->
             let st, m2 = State.update_return pb st (fun pb ->
               let m1 = LibMeta.fresh pb mk_Type 0 in
-              let m2 = LibMeta.fresh pb (mk_Meta (m1,[||])) (List.length args) in (* empty context is surely wrong *)
+              let m2 = LibMeta.fresh pb (mk_Meta (m1,[||]))
+                (List.length args) in (* empty context is surely wrong *)
               pb, m2) in
             State.update metamap st (MM.add flex m2), m2
            in

src/handle/command.ml

@@ -195,6 +195,8 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
   Console.out 3 (Color.cya "%a") Pos.pp pos;
   Console.out 4 "%a" Pretty.command cmd;
   match elt with
+  | P_elpi(file,pred,arg) ->
+      (ss, None, (Elpi_handle.run ss file pred arg; None))
   | P_query(q) -> (ss, None, Query.handle ss None q)
   | P_require(b,ps) ->
       (List.fold_left (handle_require compile b) ss ps, None, None)
@@ -547,8 +549,10 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
   | Fatal(Some(Some(_)),_) as e -> raise e
   | Fatal(None         ,m)      -> fatal pos "Error on command.@.%s" m
   | Fatal(Some(None)   ,m)      -> fatal pos "Error on command.@.%s" m
+  (*
   | e                           ->
       fatal pos "Uncaught exception: %s." (Printexc.to_string e)
+*)
 
 (** [handle compile_mod ss cmd] retrieves proof data from [cmd] (with
     {!val:get_proof_data}) and handles proofs using functions from

src/handle/elpi_handle.ml

@@ -46,7 +46,10 @@ let document () =
 let elpi = ref None
 
 let init () =
-  let e = Setup.init ~builtins:[lambdapi_builtins] ~legacy_parser:false () in
+  let e = Setup.init
+    ~builtins:[lambdapi_builtins]
+    ~legacy_parser:false
+    ~file_resolver:(Parse.std_resolver ~paths:[] ()) () in
   elpi := Some e;
   document ()
 
@@ -61,21 +64,27 @@ fun ss file predicate arg ->
 
   let ast = Parse.program ~elpi ~files:[file] in
   let prog =
-    Elpi.API.Compile.program
-      ~flags:Elpi.API.Compile.default_flags ~elpi [ast] in
+    let flags = Elpi.API.Compile.default_flags in
+    ast |>
+    Elpi.API.Compile.unit ~flags ~elpi |>
+    (fun u -> Elpi.API.Compile.assemble ~elpi ~flags [u]) in
+
   let query =
     let open Query in
-    compile prog loc (Query { predicate; arguments = D(term,arg,N) }) in
+    compile prog loc
+      (Query { predicate; arguments = (D(term,arg,Q(term,"it",N))) }) in
 
   if not (Elpi.API.Compile.static_check
             ~checker:(Elpi.Builtin.default_checker ()) query) then
     Common.Error.fatal pos "elpi: type error in %s" file;
 
   Common.Console.out 1 "\nelpi: before: %a\n" Print.term arg;
   match Execute.once (Elpi.API.Compile.optimize query) with
-  | Execute.Success { Data.state; pp_ctx; constraints; _ } ->
+  | Execute.Success {
+      Data.state; pp_ctx; constraints; output = (arg1,()); _
+    } ->
       let _ = readback_assignments state in
-      Common.Console.out 1 "\nelpi: after: %a\n" Print.term arg;
+      Common.Console.out 1 "\nelpi: after: %a\n" Print.term arg1;
       Common.Console.out 1 "elpi: constraints:@ @[<v>%a@]\n"
         Pp.(constraints pp_ctx) constraints
   | Failure -> Common.Error.fatal_no_pos "elpi: failure"

src/parsing/lpLexer.ml

@@ -45,6 +45,7 @@ type token =
   | COMPUTE
   | CONSTANT
   | DEBUG
+  | ELPI
   | END
   | FAIL
   | FLAG
@@ -208,6 +209,7 @@ let rec token lb =
   | "compute" -> COMPUTE
   | "constant" -> CONSTANT
   | "debug" -> DEBUG
+  | "elpi" -> ELPI
   | "end" -> END
   | "fail" -> FAIL
   | "flag" -> FLAG

src/parsing/lpParser.mly

@@ -38,6 +38,7 @@
 %token COMPUTE
 %token CONSTANT
 %token DEBUG
+%token ELPI
 %token END
 %token FAIL
 %token FLAG
@@ -162,6 +163,8 @@ command:
   | NOTATION i=qid_or_nat n=notation SEMICOLON
     { make_pos $loc (P_notation(i,n)) }
   | q=query SEMICOLON { make_pos $sloc (P_query(q)) }
+  | ELPI f=STRINGLIT p=STRINGLIT a=term SEMICOLON
+    { make_pos $sloc (P_elpi(f,p,a)) }
   | EOF { raise End_of_file }
 
 query:

src/parsing/syntax.ml

@@ -266,6 +266,7 @@ type p_command_aux =
   | P_unif_rule of p_rule
   | P_coercion of p_rule
   | P_query of p_query
+  | P_elpi of string * string * p_term
 
 (** Parser-level representation of a single (located) command. *)
 type p_command = p_command_aux loc

tests/OK/elpitest.elpi

@@ -1,7 +1,8 @@
-main T :-
+main T T1 :-
   print "before type inference" T,
   of T _,
-  print "\nafter type inference" T.
+  print "\nafter type inference" T,
+  T1 = T.
 
 
 pred of i:term, o:term.

tests/OK/elpitest.lp

@@ -1,6 +1,7 @@
-require open tests.OK.logic
-require open tests.OK.bool
-require open tests.OK.nat
+require open tests.OK.logic;
+require open tests.OK.bool;
+
+assert ⊢ true  : B;
 
 elpi "tests/OK/elpitest.elpi" "main"
-  (Πx y, P (eq ?T[x;y] x y) → P (eq ?T[x;y] y x))
+  (Π x y , P (x = y) → P (y = x));