Merge pull request #206 from LPCIC/state_init

API: state updater

CHANGES.md

@@ -1,5 +1,9 @@
 # UNRELEASED
 
+API:
+  - New `RawQuery.compile_ast`, lets one set up the initial state in which the
+    query is run, even if the query is given as an ast
+
 Library:
   - New `std.fold-right`
 

src/API.ml

@@ -165,7 +165,7 @@ module Compile = struct
     Compiler.program_of_ast ~flags ~header (List.flatten l)
 
   let query s_p t =
-    Compiler.query_of_ast s_p t
+    Compiler.query_of_ast s_p t (fun st -> st)
 
   let static_check ~checker q =
     let module R = (val !r) in let open R in
@@ -942,6 +942,8 @@ module RawQuery = struct
 
   let is_Arg = Compiler.is_Arg
   let compile = Compiler.query_of_term
+  let compile_ast = Compiler.query_of_ast
+
 end
 
 module Quotation = struct

src/API.mli

@@ -1067,10 +1067,16 @@ module RawQuery : sig
   (* Args are parameters of the query (e.g. capital letters). *)
   val is_Arg : State.t -> Data.term -> bool
 
+  (* with the possibility to update the state in which the query will run *)
+  val compile_ast :
+    Compile.program -> Ast.query -> (State.t -> State.t) -> unit Compile.query
+
+  (* generate the query term and initial state by hand *)
   val compile :
     Compile.program -> (depth:int -> State.t -> State.t * (Ast.Loc.t * Data.term) * Conversion.extra_goals) ->
       unit Compile.query
 
+
 end
 
 module Quotation : sig

src/compiler.ml

@@ -2229,7 +2229,7 @@ let uvbodies_of_assignments assignments =
      | UVar(b,_,_) | AppUVar(b,_,_) -> b
      | _ -> assert false) assignments)
 
-let query_of_ast (compiler_state, assembled_program) t =
+let query_of_ast (compiler_state, assembled_program) t state_update =
   let compiler_state = State.begin_goal_compilation compiler_state in
   let initial_depth = assembled_program.Assembled.local_names in
   let types = assembled_program.Assembled.types in
@@ -2256,7 +2256,7 @@ let query_of_ast (compiler_state, assembled_program) t =
     query_arguments = Query.N;
     initial_goal;
     assignments;
-    compiler_state = state |> (uvbodies_of_assignments assignments);
+    compiler_state = state |> (uvbodies_of_assignments assignments) |> state_update;
   }
 
 let query_of_term (compiler_state, assembled_program) f =

src/compiler.mli

@@ -31,7 +31,7 @@ val assemble_units : flags:flags -> header:header -> compilation_unit list -> pr
 val append_units : flags:flags -> base:program -> compilation_unit list -> program
 
 type 'a query
-val query_of_ast : program -> Ast.Goal.t -> unit query
+val query_of_ast : program -> Ast.Goal.t -> (State.t -> State.t) -> unit query
 val query_of_term :
   program -> (depth:int -> State.t -> State.t * (Loc.t * term) * Conversion.extra_goals) -> unit query
 val query_of_data :