diff --git a/src/.ppcache/API.ml b/src/.ppcache/API.ml deleted file mode 100644 index add18dbb2..000000000 --- a/src/.ppcache/API.ml +++ /dev/null @@ -1,1430 +0,0 @@ -(*3945de0aacc72f43356fcba834b89bc2bd5836f5 *src/API.ml --cookie elpi_trace="false"*) -#1 "src/API.ml" -module type Runtime = module type of Runtime_trace_off -let r = ref ((module Runtime_trace_off) : (module Runtime)) -let set_runtime b = - (match b with - | true -> r := ((module Runtime_trace_on) : (module Runtime)) - | false -> r := ((module Runtime_trace_off) : (module Runtime))); - (let module R = (val !r) in - Util.set_spaghetti_printer Data.pp_const R.Pp.pp_constant) -let set_trace argv = - let args = Trace_ppx_runtime.Runtime.parse_argv argv in - set_runtime (!Trace_ppx_runtime.Runtime.debug); args -module Setup = - struct - type builtins = (string * Data.BuiltInPredicate.declaration list) - type elpi = (Parser.parser_state * Compiler.compilation_unit) - let init ~builtins ~basedir:cwd argv = - let new_argv = set_trace argv in - let (new_argv, paths) = - let rec aux args paths = - function - | [] -> ((List.rev args), (List.rev paths)) - | "-I"::p::rest -> aux args (p :: paths) rest - | x::rest -> aux (x :: args) paths rest in - aux [] [] new_argv in - let parsing_state = - Parser.init ~lp_syntax:Parser.lp_gramext ~paths ~cwd in - let state = Compiler.init_state Compiler.default_flags in - let state = - List.fold_left - (fun state -> - fun (_, decls) -> - List.fold_left - (fun state -> - function - | Data.BuiltInPredicate.MLCode (p, _) -> - Compiler.Builtins.register state p - | Data.BuiltInPredicate.MLData _ -> state - | Data.BuiltInPredicate.LPCode _ -> state - | Data.BuiltInPredicate.LPDoc _ -> state) state decls) - state builtins in - let header = - builtins |> - (List.map - (fun (fname, decls) -> - let b = Buffer.create 1024 in - let fmt = Format.formatter_of_buffer b in - Data.BuiltInPredicate.document fmt decls; - Format.pp_print_flush fmt (); - (let text = Buffer.contents b in - let strm = Stream.of_string text in - let loc = Util.Loc.initial fname in - try - Parser.parse_program_from_stream parsing_state - ~print_accumulated_files:false loc strm - with - | Parser.ParseError (loc, msg) -> - (List.iteri - (fun i -> - fun s -> Printf.eprintf "%4d: %s\n" (i + 1) s) - (let open Re.Str in - split_delim (regexp_string "\n") text); - Printf.eprintf "Excerpt of %s:\n%s\n" fname - (String.sub text loc.Util.Loc.line_starts_at - (let open Util.Loc in - loc.source_stop - loc.line_starts_at)); - Util.anomaly ~loc msg)))) in - let header = - try Compiler.unit_of_ast state (List.concat header) - with | Compiler.CompileError (loc, msg) -> Util.anomaly ?loc msg in - ((parsing_state, header), new_argv) - let trace args = - match set_trace args with - | [] -> () - | l -> - Util.error - ("Elpi_API.trace got unknown arguments: " ^ (String.concat " " l)) - let usage = - "\nParsing options:\n" ^ - ("\t-I PATH search for accumulated files in PATH\n" ^ - Trace_ppx_runtime.Runtime.usage) - let set_warn = Util.set_warn - let set_error = Util.set_error - let set_anomaly = Util.set_anomaly - let set_type_error = Util.set_type_error - let set_std_formatter = Util.set_std_formatter - let set_err_formatter fmt = - Util.set_err_formatter fmt; - (let open Trace_ppx_runtime.Runtime in set_trace_output TTY fmt) - end -module EA = Ast -module Ast = - struct - type program = Ast.Program.t - type query = Ast.Goal.t - module Loc = Util.Loc - end -module Parse = - struct - let program ~elpi:(ps, _) ?(print_accumulated_files= false) = - Parser.parse_program ps ~print_accumulated_files - let program_from_stream ~elpi:(ps, _) ?(print_accumulated_files= false) - = Parser.parse_program_from_stream ps ~print_accumulated_files - let goal loc s = Parser.parse_goal ~loc s - let goal_from_stream loc s = Parser.parse_goal_from_stream ~loc s - exception ParseError = Parser.ParseError - end -module ED = Data -module Data = - struct - type term = Data.term - type constraints = Data.constraints - type state = Data.State.t - type pretty_printer_context = ED.pp_ctx - type constant = Data.constant - module StrMap = Util.StrMap - type 'a solution = 'a Data.solution = - { - assignments: term StrMap.t ; - constraints: constraints ; - state: state ; - output: 'a ; - pp_ctx: pretty_printer_context } - type hyp = Data.clause_src = { - hdepth: int ; - hsrc: term } - type hyps = hyp list - module Constants = struct module Map = Data.Constants.Map end - end -module Compile = - struct - type program = (ED.State.t * Compiler.program) - type 'a query = 'a Compiler.query - type 'a executable = 'a ED.executable - type compilation_unit = Compiler.compilation_unit - exception CompileError = Compiler.CompileError - let program ~flags ~elpi:(_, header) l = - Compiler.program_of_ast (Compiler.init_state flags) ~header - (List.flatten l) - let query (s, p) t = Compiler.query_of_ast s p t - let static_check ~checker q = - let module R = (val !r) in - let open R in - Compiler.static_check - ~exec:(execute_once ~delay_outside_fragment:false) ~checker q - module StrSet = Util.StrSet - type flags = Compiler.flags = - { - defined_variables: StrSet.t ; - print_passes: bool } - let default_flags = Compiler.default_flags - let optimize = Compiler.optimize_query - let unit ~elpi:(_, header) ~flags x = - Compiler.unit_of_ast (Compiler.init_state flags) ~header x - let assemble ~elpi:(_, header) = Compiler.assemble_units ~header - end -module Execute = - struct - type 'a outcome = 'a ED.outcome = - | Success of 'a Data.solution - | Failure - | NoMoreSteps - let once ?max_steps ?delay_outside_fragment p = - let module R = (val !r) in - R.execute_once ?max_steps ?delay_outside_fragment p - let loop ?delay_outside_fragment p ~more ~pp = - let module R = (val !r) in - R.execute_loop ?delay_outside_fragment p ~more ~pp - end -module Pp = - struct - let term pp_ctx f t = - let module R = (val !r) in - let open R in R.Pp.uppterm ~pp_ctx 0 [] 0 [||] f t - let constraints pp_ctx f c = - let module R = (val !r) in - let open R in - Util.pplist ~boxed:true (let open R in pp_stuck_goal ~pp_ctx) "" f - c - let state = ED.State.pp - let query f c = - let module R = (val !r) in - let open R in - Compiler.pp_query (fun ~depth -> R.Pp.uppterm depth [] 0 [||]) f c - module Ast = struct let program = EA.Program.pp end - end -module Conversion = - struct - type extra_goals = ED.extra_goals - include ED.Conversion - let (^^) t = - { - t with - embed = - (fun ~depth -> - fun h -> - fun c -> - fun s -> fun x -> t.embed ~depth ((new ctx) h#raw) c s x); - readback = - (fun ~depth -> - fun h -> - fun c -> - fun s -> fun x -> t.readback ~depth ((new ctx) h#raw) c s x) - } - end -module OpaqueData = - struct - include Util.CData - include ED.C - type name = string - type doc = string - type 'a declaration = - { - name: name ; - cname: name ; - doc: doc ; - pp: Format.formatter -> 'a -> unit ; - compare: 'a -> 'a -> int ; - hash: 'a -> int ; - hconsed: bool ; - constants: (name * 'a) list } - type 'a cdata_with_constants = - ('a cdata * name * (string * 'a) ED.Constants.Map.t * doc) - let rest ({ cin; name = c }, name, constants_map, doc) = - ((Conversion.TyName name), (fun fmt -> fun x -> pp fmt (cin x)), - (fun fmt -> - fun () -> - let module R = (val !r) in - let open R in - if doc <> "" - then - (ED.BuiltInPredicate.pp_comment fmt ("% " ^ doc); - Format.fprintf fmt "@\n"); - Format.fprintf fmt - "@[typeabbrev %s (ctype \"%s\").@]@\n@\n" name c; - ED.Constants.Map.iter - (fun _ -> - fun (c, _) -> - Format.fprintf fmt "@[type %s %s.@]@\n" c name) - constants_map)) - let embed ({ cin;_}, _, _, _) = - (); - (fun ~depth:_ -> - fun _ -> - fun _ -> - fun state -> fun x -> (state, (ED.Term.CData (cin x)), [])) - let readback ({ isc; cout;_}, name, constants_map, _) = - (); - (fun ~depth -> - fun _ -> - fun _ -> - fun state -> - fun t -> - let module R = (val !r) in - let open R in - match R.deref_head ~depth t with - | ED.Term.CData c when isc c -> (state, (cout c), []) - | ED.Term.Const i as t when i < 0 -> - (try - (state, - (snd @@ (ED.Constants.Map.find i constants_map)), - []) - with - | Not_found -> - raise - (Conversion.TypeErr - ((Conversion.TyName name), depth, t))) - | t -> - raise - (Conversion.TypeErr - ((Conversion.TyName name), depth, t))) - let declare { name; cname; doc; pp; compare; hash; hconsed; constants } = - let cdata = - declare - { - data_compare = compare; - data_pp = pp; - data_hash = hash; - data_name = cname; - data_hconsed = hconsed - } in - (cdata, name, - (List.fold_right - (fun (n, v) -> - ED.Constants.Map.add - (ED.Global_symbols.declare_global_symbol n) (n, v)) constants - ED.Constants.Map.empty), doc) - let build_conversion x = - let (ty, pp, pp_doc) = rest x in - { - Conversion.ty = ty; - pp; - pp_doc; - embed = (embed x); - readback = (readback x) - } - end -module RawOpaqueData = - struct - include Util.CData - include ED.C - let cdata (c, _, _, _) = c - let { cin = of_char; isc = is_char; cout = to_char } as char = - declare - { - data_compare = Pervasives.compare; - data_pp = (fun fmt -> fun c -> Format.fprintf fmt "%c" c); - data_hash = Hashtbl.hash; - data_name = "char"; - data_hconsed = false - } - let of_char x = ED.mkCData (of_char x) - let { cin = of_out_stream; isc = is_out_stream; cout = to_out_stream } as - out_stream - = - declare - { - data_compare = (fun (_, s1) -> fun (_, s2) -> String.compare s1 s2); - data_pp = - (fun fmt -> fun (_, d) -> Format.fprintf fmt "" d); - data_hash = (fun (x, _) -> Hashtbl.hash x); - data_name = "out_stream"; - data_hconsed = false - } - let of_out_stream x = ED.mkCData (of_out_stream x) - let { cin = of_in_stream; isc = is_in_stream; cout = to_in_stream } as - in_stream - = - declare - { - data_compare = (fun (_, s1) -> fun (_, s2) -> String.compare s1 s2); - data_pp = - (fun fmt -> fun (_, d) -> Format.fprintf fmt "" d); - data_hash = (fun (x, _) -> Hashtbl.hash x); - data_name = "in_stream"; - data_hconsed = false - } - let of_in_stream x = ED.mkCData (of_in_stream x) - end -module Elpi = - struct - type t = - | Arg of string - | Ref of ED.uvar_body - let pp fmt handle = - match handle with - | Arg str -> Format.fprintf fmt "%s" str - | Ref ub -> - let module R = (val !r) in - let open R in R.Pp.uppterm 0 [] 0 [||] fmt (ED.mkUVar ub 0 0) - let show m = Format.asprintf "%a" pp m - let equal h1 h2 = - match (h1, h2) with - | (Ref p1, Ref p2) -> p1 == p2 - | (Arg s1, Arg s2) -> String.equal s1 s2 - | _ -> false - let compilation_is_over ~args k = - match k with - | Ref _ -> assert false - | Arg s -> Ref (Util.StrMap.find s args) - let uvk = - ED.State.declare ~name:"elpi:uvk" ~pp:(Util.StrMap.pp pp) - ~clause_compilation_is_over:(fun x -> Util.StrMap.empty) - ~goal_compilation_is_over:(fun ~args -> - fun x -> - Some - (Util.StrMap.map - (compilation_is_over ~args) x)) - ~compilation_is_over:(fun _ -> None) - ~execution_is_over:(fun _ -> None) - ~init:(fun () -> Util.StrMap.empty) - let fresh_name = - let i = ref 0 in fun () -> incr i; Printf.sprintf "_uvk_%d_" (!i) - let alloc_Elpi name state = - if ED.State.get ED.while_compiling state - then - let (state, _arg) = Compiler.mk_Arg ~name ~args:[] state in - (state, (Arg name)) - else (let module R = (val !r) in (state, (Ref (ED.oref ED.dummy)))) - let make ?name state = - match name with - | None -> alloc_Elpi (fresh_name ()) state - | Some name -> - (try (state, (Util.StrMap.find name (ED.State.get uvk state))) - with - | Not_found -> - let (state, k) = alloc_Elpi name state in - ((ED.State.update uvk state (Util.StrMap.add name k)), k)) - let get ~name state = - try Some (Util.StrMap.find name (ED.State.get uvk state)) - with | Not_found -> None - end -module RawData = - struct - type constant = ED.Term.constant - type builtin = ED.Term.constant - type uvar_body = ED.Term.uvar_body - type term = ED.Term.term - type view = - | Const of constant - | Lam of term - | App of constant * term * term list - | Cons of term * term - | Nil - | Builtin of builtin * term list - | CData of RawOpaqueData.t - | UnifVar of Elpi.t * term list - let rec look ~depth t = - let module R = (val !r) in - let open R in - match R.deref_head ~depth t with - | ED.Term.Arg _|ED.Term.AppArg _ -> assert false - | ED.Term.AppUVar (ub, 0, args) -> UnifVar ((Ref ub), args) - | ED.Term.AppUVar (ub, lvl, args) -> - look ~depth (R.expand_appuv ub ~depth ~lvl ~args) - | ED.Term.UVar (ub, lvl, ano) -> - look ~depth (R.expand_uv ub ~depth ~lvl ~ano) - | ED.Term.Discard -> - let ub = ED.oref ED.dummy in - UnifVar ((Ref ub), (R.mkinterval 0 depth 0)) - | x -> Obj.magic x - let kool = - function - | UnifVar (Ref ub, args) -> ED.Term.AppUVar (ub, 0, args) - | UnifVar (Arg _, _) -> assert false - | x -> Obj.magic x[@@inline ] - let mkConst n = let module R = (val !r) in R.mkConst n - let mkLam = ED.Term.mkLam - let mkApp = ED.Term.mkApp - let mkCons = ED.Term.mkCons - let mkNil = ED.Term.mkNil - let mkDiscard = ED.Term.mkDiscard - let mkBuiltin = ED.Term.mkBuiltin - let mkCData = ED.Term.mkCData - let mkAppL x l = let module R = (val !r) in R.mkAppL x l - let mkGlobal i = - if i >= 0 then Util.anomaly "mkGlobal: got a bound variable"; mkConst i - let mkBound i = - if i < 0 then Util.anomaly "mkBound: got a global constant"; mkConst i - let cmp_builtin i j = i - j - module Constants = - struct - let declare_global_symbol = ED.Global_symbols.declare_global_symbol - let show c = ED.Constants.show c - let eqc = ED.Global_symbols.eqc - let orc = ED.Global_symbols.orc - let andc = ED.Global_symbols.andc - let rimplc = ED.Global_symbols.rimplc - let pic = ED.Global_symbols.pic - let sigmac = ED.Global_symbols.sigmac - let implc = ED.Global_symbols.implc - let cutc = ED.Global_symbols.cutc - let ctypec = ED.Global_symbols.ctypec - let spillc = ED.Global_symbols.spillc - module Map = ED.Constants.Map - module Set = ED.Constants.Set - end - let of_term x = x - type suspended_goal = ED.suspended_goal = - { - context: Data.hyps ; - goal: (int * term) } - type constraints = Data.constraints - let constraints l = - let module R = (val !r) in - let open R in - Util.map_filter (fun x -> R.get_suspended_goal x.ED.kind) l - let no_constraints = [] - let mkUnifVar handle ~args state = - match handle with - | Elpi.Ref ub -> ED.Term.mkAppUVar ub 0 args - | Elpi.Arg name -> Compiler.get_Arg state ~name ~args - end -module FlexibleData = - struct - module Elpi = Elpi - module type Host = - sig - type t - val compare : t -> t -> int - val pp : Format.formatter -> t -> unit - val show : t -> string - end - let uvmap_no = ref 0 - module Map(T:Host) = - struct - open Util - module H2E = (Map.Make)(T) - type t = - { - h2e: Elpi.t H2E.t ; - e2h_compile: T.t StrMap.t ; - e2h_run: T.t PtrMap.t } - let empty = - { - h2e = H2E.empty; - e2h_compile = StrMap.empty; - e2h_run = (PtrMap.empty ()) - } - let add uv v { h2e; e2h_compile; e2h_run } = - let h2e = H2E.add v uv h2e in - match uv with - | Elpi.Ref ub -> - { h2e; e2h_compile; e2h_run = (PtrMap.add ub v e2h_run) } - | Arg s -> - { h2e; e2h_run; e2h_compile = (StrMap.add s v e2h_compile) } - let elpi v { h2e } = H2E.find v h2e - let host handle { e2h_compile; e2h_run } = - match handle with - | Elpi.Ref ub -> PtrMap.find ub e2h_run - | Arg s -> StrMap.find s e2h_compile - let remove_both handle v { h2e; e2h_compile; e2h_run } = - let h2e = H2E.remove v h2e in - match handle with - | Elpi.Ref ub -> - { h2e; e2h_compile; e2h_run = (PtrMap.remove ub e2h_run) } - | Arg s -> - { h2e; e2h_run; e2h_compile = (StrMap.remove s e2h_compile) } - let remove_elpi k m = let v = host k m in remove_both k v m - let remove_host v m = let handle = elpi v m in remove_both handle v m - let filter f { h2e; e2h_compile; e2h_run } = - let e2h_compile = - StrMap.filter (fun n -> fun v -> f v (H2E.find v h2e)) - e2h_compile in - let e2h_run = - PtrMap.filter (fun ub -> fun v -> f v (H2E.find v h2e)) e2h_run in - let h2e = H2E.filter f h2e in { h2e; e2h_compile; e2h_run } - let fold f { h2e } acc = - let module R = (val !r) in - let open R in - let get_val = - function - | Elpi.Ref { ED.Term.contents = ub } when ub != ED.dummy -> - Some (R.deref_head ~depth:0 ub) - | Elpi.Ref _ -> None - | Elpi.Arg _ -> None in - H2E.fold - (fun k -> fun uk -> fun acc -> f k uk (get_val uk) acc) h2e - acc - let uvn = incr uvmap_no; !uvmap_no - let pp fmt (m : t) = - let pp k uv _ () = - Format.fprintf fmt "@[%a@ <-> %a@]@ " T.pp k Elpi.pp uv in - Format.fprintf fmt "@["; fold pp m (); Format.fprintf fmt "@]" - let show m = Format.asprintf "%a" pp m - let uvmap = - ED.State.declare ~name:(Printf.sprintf "elpi:uvm:%d" uvn) ~pp - ~clause_compilation_is_over:(fun x -> empty) - ~goal_compilation_is_over:(fun ~args -> - fun { h2e; e2h_compile; e2h_run } -> - let h2e = - H2E.map - (Elpi.compilation_is_over - ~args) h2e in - let e2h_run = - StrMap.fold - (fun k -> - fun v -> - fun m -> - PtrMap.add - (StrMap.find k args) - v m) e2h_compile - (PtrMap.empty ()) in - Some - { - h2e; - e2h_compile = StrMap.empty; - e2h_run - }) - ~compilation_is_over:(fun x -> Some x) - ~execution_is_over:(fun x -> Some x) ~init:(fun () -> empty) - end - let uvar = - { - Conversion.ty = (Conversion.TyName "uvar"); - pp_doc = - (fun fmt -> - fun () -> - Format.fprintf fmt "Unification variable, as the uvar keyword"); - pp = (fun fmt -> fun (k, _) -> Format.fprintf fmt "%a" Elpi.pp k); - embed = - (fun ~depth -> - fun _ -> - fun _ -> - fun s -> - fun (k, args) -> (s, (RawData.mkUnifVar k ~args s), [])); - readback = - (fun ~depth -> - fun _ -> - fun _ -> - fun state -> - fun t -> - match RawData.look ~depth t with - | RawData.UnifVar (k, args) -> (state, (k, args), []) - | _ -> - raise - (Conversion.TypeErr ((TyName "uvar"), depth, t))) - } - end -module BuiltIn = - struct - include ED.BuiltInPredicate - let declare ~file_name l = (file_name, l) - let document_fmt fmt (_, l) = ED.BuiltInPredicate.document fmt l - let document_file ?(header= "") (name, l) = - let oc = open_out name in - let fmt = Format.formatter_of_out_channel oc in - Format.fprintf fmt "%s%!" header; - ED.BuiltInPredicate.document fmt l; - Format.pp_print_flush fmt (); - close_out oc - end -module BuiltInData = - struct - let () = () - let int : 'h . (int, 'h) Conversion.t = - let name = "int" in - let doc = "" in - let cdata = ED.C.int in - let constants = [] in - let constants_map = ED.Constants.Map.empty in - let { Util.CData.cin = cin; isc; cout; name = c } = cdata in - let ty = Conversion.TyName name in - let embed ~depth:_ _ _ state x = (state, (ED.Term.CData (cin x)), []) in - let readback ~depth _ _ state t = - let module R = (val !r) in - let open R in - match R.deref_head ~depth t with - | ED.Term.CData c when isc c -> (state, (cout c), []) - | ED.Term.Const i as t when i < 0 -> - (try (state, (ED.Constants.Map.find i constants_map), []) - with - | Not_found -> raise (Conversion.TypeErr (ty, depth, t))) - | t -> raise (Conversion.TypeErr (ty, depth, t)) in - let pp_doc fmt () = - let module R = (val !r) in - let open R in - if doc <> "" - then - (ED.BuiltInPredicate.pp_comment fmt ("% " ^ doc); - Format.fprintf fmt "@\n"); - Format.fprintf fmt - "@[typeabbrev %s (ctype \"%s\").@]@\n@\n" name c; - List.iter - (fun (c, _) -> - Format.fprintf fmt "@[type %s %s.@]@\n" c name) - constants in - { - Conversion.embed = embed; - readback; - ty; - pp_doc; - pp = (fun fmt -> fun x -> Util.CData.pp fmt (cin x)) - } - let float : 'h . (float, 'h) Conversion.t = - let name = "float" in - let doc = "" in - let cdata = ED.C.float in - let constants = [] in - let constants_map = ED.Constants.Map.empty in - let { Util.CData.cin = cin; isc; cout; name = c } = cdata in - let ty = Conversion.TyName name in - let embed ~depth:_ _ _ state x = (state, (ED.Term.CData (cin x)), []) in - let readback ~depth _ _ state t = - let module R = (val !r) in - let open R in - match R.deref_head ~depth t with - | ED.Term.CData c when isc c -> (state, (cout c), []) - | ED.Term.Const i as t when i < 0 -> - (try (state, (ED.Constants.Map.find i constants_map), []) - with - | Not_found -> raise (Conversion.TypeErr (ty, depth, t))) - | t -> raise (Conversion.TypeErr (ty, depth, t)) in - let pp_doc fmt () = - let module R = (val !r) in - let open R in - if doc <> "" - then - (ED.BuiltInPredicate.pp_comment fmt ("% " ^ doc); - Format.fprintf fmt "@\n"); - Format.fprintf fmt - "@[typeabbrev %s (ctype \"%s\").@]@\n@\n" name c; - List.iter - (fun (c, _) -> - Format.fprintf fmt "@[type %s %s.@]@\n" c name) - constants in - { - Conversion.embed = embed; - readback; - ty; - pp_doc; - pp = (fun fmt -> fun x -> Util.CData.pp fmt (cin x)) - } - let string : 'h . (string, 'h) Conversion.t = - let name = "string" in - let doc = "" in - let cdata = ED.C.string in - let constants = [] in - let constants_map = ED.Constants.Map.empty in - let { Util.CData.cin = cin; isc; cout; name = c } = cdata in - let ty = Conversion.TyName name in - let embed ~depth:_ _ _ state x = (state, (ED.Term.CData (cin x)), []) in - let readback ~depth _ _ state t = - let module R = (val !r) in - let open R in - match R.deref_head ~depth t with - | ED.Term.CData c when isc c -> (state, (cout c), []) - | ED.Term.Const i as t when i < 0 -> - (try (state, (ED.Constants.Map.find i constants_map), []) - with - | Not_found -> raise (Conversion.TypeErr (ty, depth, t))) - | t -> raise (Conversion.TypeErr (ty, depth, t)) in - let pp_doc fmt () = - let module R = (val !r) in - let open R in - if doc <> "" - then - (ED.BuiltInPredicate.pp_comment fmt ("% " ^ doc); - Format.fprintf fmt "@\n"); - Format.fprintf fmt - "@[typeabbrev %s (ctype \"%s\").@]@\n@\n" name c; - List.iter - (fun (c, _) -> - Format.fprintf fmt "@[type %s %s.@]@\n" c name) - constants in - { - Conversion.embed = embed; - readback; - ty; - pp_doc; - pp = (fun fmt -> fun x -> Util.CData.pp fmt (cin x)) - } - let loc : 'h . (Util.Loc.t, 'h) Conversion.t = - let name = "loc" in - let doc = "" in - let cdata = ED.C.loc in - let constants = [] in - let constants_map = ED.Constants.Map.empty in - let { Util.CData.cin = cin; isc; cout; name = c } = cdata in - let ty = Conversion.TyName name in - let embed ~depth:_ _ _ state x = (state, (ED.Term.CData (cin x)), []) in - let readback ~depth _ _ state t = - let module R = (val !r) in - let open R in - match R.deref_head ~depth t with - | ED.Term.CData c when isc c -> (state, (cout c), []) - | ED.Term.Const i as t when i < 0 -> - (try (state, (ED.Constants.Map.find i constants_map), []) - with - | Not_found -> raise (Conversion.TypeErr (ty, depth, t))) - | t -> raise (Conversion.TypeErr (ty, depth, t)) in - let pp_doc fmt () = - let module R = (val !r) in - let open R in - if doc <> "" - then - (ED.BuiltInPredicate.pp_comment fmt ("% " ^ doc); - Format.fprintf fmt "@\n"); - Format.fprintf fmt - "@[typeabbrev %s (ctype \"%s\").@]@\n@\n" name c; - List.iter - (fun (c, _) -> - Format.fprintf fmt "@[type %s %s.@]@\n" c name) - constants in - { - Conversion.embed = embed; - readback; - ty; - pp_doc; - pp = (fun fmt -> fun x -> Util.CData.pp fmt (cin x)) - } - let char : 'h . (char, 'h) Conversion.t = - let name = "char" in - let doc = "an octect" in - let cdata = RawOpaqueData.char in - let constants = [] in - let constants_map = ED.Constants.Map.empty in - let { Util.CData.cin = cin; isc; cout; name = c } = cdata in - let ty = Conversion.TyName name in - let embed ~depth:_ _ _ state x = (state, (ED.Term.CData (cin x)), []) in - let readback ~depth _ _ state t = - let module R = (val !r) in - let open R in - match R.deref_head ~depth t with - | ED.Term.CData c when isc c -> (state, (cout c), []) - | ED.Term.Const i as t when i < 0 -> - (try (state, (ED.Constants.Map.find i constants_map), []) - with - | Not_found -> raise (Conversion.TypeErr (ty, depth, t))) - | t -> raise (Conversion.TypeErr (ty, depth, t)) in - let pp_doc fmt () = - let module R = (val !r) in - let open R in - if doc <> "" - then - (ED.BuiltInPredicate.pp_comment fmt ("% " ^ doc); - Format.fprintf fmt "@\n"); - Format.fprintf fmt - "@[typeabbrev %s (ctype \"%s\").@]@\n@\n" name c; - List.iter - (fun (c, _) -> - Format.fprintf fmt "@[type %s %s.@]@\n" c name) - constants in - { - Conversion.embed = embed; - readback; - ty; - pp_doc; - pp = (fun fmt -> fun x -> Util.CData.pp fmt (cin x)) - } - let in_stream_constants = [("std_in", (stdin, "stdin"))] - let in_stream_cmap = - List.fold_left - (fun m -> - fun (c, v) -> - let c = ED.Global_symbols.declare_global_symbol c in - ED.Constants.Map.add c v m) ED.Constants.Map.empty - in_stream_constants - let in_stream : 'h . ((in_channel * string), 'h) Conversion.t = - let name = "in_stream" in - let doc = "" in - let cdata = RawOpaqueData.in_stream in - let constants = in_stream_constants in - let constants_map = in_stream_cmap in - let { Util.CData.cin = cin; isc; cout; name = c } = cdata in - let ty = Conversion.TyName name in - let embed ~depth:_ _ _ state x = (state, (ED.Term.CData (cin x)), []) in - let readback ~depth _ _ state t = - let module R = (val !r) in - let open R in - match R.deref_head ~depth t with - | ED.Term.CData c when isc c -> (state, (cout c), []) - | ED.Term.Const i as t when i < 0 -> - (try (state, (ED.Constants.Map.find i constants_map), []) - with - | Not_found -> raise (Conversion.TypeErr (ty, depth, t))) - | t -> raise (Conversion.TypeErr (ty, depth, t)) in - let pp_doc fmt () = - let module R = (val !r) in - let open R in - if doc <> "" - then - (ED.BuiltInPredicate.pp_comment fmt ("% " ^ doc); - Format.fprintf fmt "@\n"); - Format.fprintf fmt - "@[typeabbrev %s (ctype \"%s\").@]@\n@\n" name c; - List.iter - (fun (c, _) -> - Format.fprintf fmt "@[type %s %s.@]@\n" c name) - constants in - { - Conversion.embed = embed; - readback; - ty; - pp_doc; - pp = (fun fmt -> fun x -> Util.CData.pp fmt (cin x)) - } - let out_stream_constants = - [("std_out", (stdout, "stdout")); ("std_err", (stderr, "stderr"))] - let out_stream_cmap = - List.fold_left - (fun m -> - fun (c, v) -> - let c = ED.Global_symbols.declare_global_symbol c in - ED.Constants.Map.add c v m) ED.Constants.Map.empty - out_stream_constants - let out_stream : 'h . ((out_channel * string), 'h) Conversion.t = - let name = "out_stream" in - let doc = "" in - let cdata = RawOpaqueData.out_stream in - let constants = out_stream_constants in - let constants_map = out_stream_cmap in - let { Util.CData.cin = cin; isc; cout; name = c } = cdata in - let ty = Conversion.TyName name in - let embed ~depth:_ _ _ state x = (state, (ED.Term.CData (cin x)), []) in - let readback ~depth _ _ state t = - let module R = (val !r) in - let open R in - match R.deref_head ~depth t with - | ED.Term.CData c when isc c -> (state, (cout c), []) - | ED.Term.Const i as t when i < 0 -> - (try (state, (ED.Constants.Map.find i constants_map), []) - with - | Not_found -> raise (Conversion.TypeErr (ty, depth, t))) - | t -> raise (Conversion.TypeErr (ty, depth, t)) in - let pp_doc fmt () = - let module R = (val !r) in - let open R in - if doc <> "" - then - (ED.BuiltInPredicate.pp_comment fmt ("% " ^ doc); - Format.fprintf fmt "@\n"); - Format.fprintf fmt - "@[typeabbrev %s (ctype \"%s\").@]@\n@\n" name c; - List.iter - (fun (c, _) -> - Format.fprintf fmt "@[type %s %s.@]@\n" c name) - constants in - { - Conversion.embed = embed; - readback; - ty; - pp_doc; - pp = (fun fmt -> fun x -> Util.CData.pp fmt (cin x)) - } - let poly ty = - let embed ~depth:_ _ _ state x = (state, x, []) in - let readback ~depth _ _ state t = (state, t, []) in - { - Conversion.embed = embed; - readback; - ty = (Conversion.TyName ty); - pp = (fun fmt -> fun _ -> Format.fprintf fmt ""); - pp_doc = (fun fmt -> fun () -> ()) - } - let any = - let embed ~depth:_ _ _ state x = (state, x, []) in - let readback ~depth _ _ state t = (state, t, []) in - { - Conversion.embed = embed; - readback; - ty = (Conversion.TyName "any"); - pp = (fun fmt -> fun _ -> Format.fprintf fmt ""); - pp_doc = (fun fmt -> fun () -> ()) - } - let nominal = - let embed ~depth:_ _ _ state x = - let module R = (val !r) in - let open R in - if x < 0 then Util.type_error "not a bound variable"; - (state, (R.mkConst x), []) in - let readback ~depth _ _ state t = - let module R = (val !r) in - let open R in - match deref_head ~depth t with - | ED.Const i when i >= 0 -> (state, i, []) - | _ -> Util.type_error "not a bound variable" in - { - Conversion.embed = embed; - readback; - ty = (TyName "nominal"); - pp = (fun fmt -> fun d -> Format.fprintf fmt "%d" d); - pp_doc = (fun fmt -> fun () -> ()) - } - let fresh_copy t depth = - let module R = (val !r) in - let open R in - let open ED in - let rec aux d t = - match deref_head ~depth:(depth + d) t with - | Lam t -> mkLam (aux (d + 1) t) - | Const c as x -> - if (c < 0) || (c >= depth) - then x - else - raise - (let open Conversion in - TypeErr ((TyName "closed term"), (depth + d), x)) - | App (c, x, xs) -> - if (c < 0) || (c >= depth) - then mkApp c (aux d x) (List.map (aux d) xs) - else - raise - (let open Conversion in - TypeErr ((TyName "closed term"), (depth + d), x)) - | UVar _|AppUVar _ as x -> - raise - (let open Conversion in - TypeErr ((TyName "closed term"), (depth + d), x)) - | Arg _|AppArg _ -> assert false - | Builtin (c, xs) -> mkBuiltin c (List.map (aux d) xs) - | CData _ as x -> x - | Cons (hd, tl) -> mkCons (aux d hd) (aux d tl) - | Nil as x -> x - | Discard as x -> x in - ((aux 0 t), depth) - let closed ty = - let ty = let open Conversion in TyName ty in - let embed ~depth _ _ state (x, from) = - let module R = (val !r) in - let open R in (state, (R.hmove ~from ~to_:depth ?avoid:None x), []) in - let readback ~depth _ _ state t = (state, (fresh_copy t depth), []) in - { - Conversion.embed = embed; - readback; - ty; - pp = - (fun fmt -> - fun (t, d) -> - let module R = (val !r) in - let open R in R.Pp.uppterm d [] d ED.empty_env fmt t); - pp_doc = (fun fmt -> fun () -> ()) - } - let map_acc f s l = - let rec aux acc extra s = - function - | [] -> (s, (List.rev acc), (let open List in concat (rev extra))) - | x::xs -> - let (s, x, gls) = f s x in aux (x :: acc) (gls :: extra) s xs in - aux [] [] s l - let embed_list d ~depth h c s l = - let module R = (val !r) in - let open R in - let (s, l, eg) = map_acc (d ~depth h c) s l in - (s, (list_to_lp_list l), eg) - let readback_list d ~depth h c s t = - let module R = (val !r) in - let open R in map_acc (d ~depth h c) s (lp_list_to_list ~depth t) - let list d = - let pp fmt l = - Format.fprintf fmt "[%a]" - (Util.pplist d.Conversion.pp ~boxed:true "; ") l in - { - Conversion.embed = (embed_list d.Conversion.embed); - readback = (readback_list d.Conversion.readback); - ty = (TyApp ("list", (d.ty), [])); - pp; - pp_doc = (fun fmt -> fun () -> ()) - } - let ttc = ED.Global_symbols.declare_global_symbol "tt" - let ffc = ED.Global_symbols.declare_global_symbol "ff" - let readback_bool ~depth h c s t = - let module R = (val !r) in - let open R in - match R.deref_head ~depth t with - | ED.Const c when c == ttc -> (s, true, []) - | ED.Const c when c == ffc -> (s, false, []) - | _ -> - raise - (let open Conversion in TypeErr ((TyName "bool"), depth, t)) - let embed_bool ~depth h c s t = - let module R = (val !r) in - let open R in - match t with - | true -> (s, (R.mkConst ttc), []) - | false -> (s, (R.mkConst ffc), []) - let bool : 'c . (bool, #Conversion.ctx as 'c) Conversion.t = - { - Conversion.ty = (Conversion.TyName "bool"); - pp_doc = - (fun fmt -> - fun () -> - ED.BuiltInPredicate.ADT.document_adt - "Boolean values: tt and ff since true and false are predicates" - (let open Conversion in TyName "bool") - [("tt", "", ["bool"]); ("ff", "", ["bool"])] fmt ()); - pp = (fun fmt -> fun b -> Format.fprintf fmt "%b" b); - embed = embed_bool; - readback = readback_bool - } - type diagnostic = - | OK - | ERROR of string BuiltIn.ioarg - let mkOK = OK - let mkERROR s = ERROR (Data s) - let okc = ED.Global_symbols.declare_global_symbol "ok" - let errorc = ED.Global_symbols.declare_global_symbol "error" - let readback_diagnostic ~depth h c s t = - let module R = (val !r) in - let open R in - match R.deref_head ~depth t with - | ED.Const c when c == okc -> (s, OK, []) - | ED.App (c, x, []) when c == errorc -> - (match R.deref_head ~depth x with - | ED.UVar _|ED.AppUVar _|ED.Discard -> (s, (ERROR NoData), []) - | ED.CData c when RawOpaqueData.is_string c -> - (s, (ERROR (Data (RawOpaqueData.to_string c))), []) - | _ -> - raise - (let open Conversion in - TypeErr ((TyName "diagnostic"), depth, t))) - | _ -> - raise - (let open Conversion in - TypeErr ((TyName "diagnostic"), depth, t)) - let embed_diagnostic ~depth h c s t = - let module R = (val !r) in - let open R in - match t with - | OK -> (s, (R.mkConst okc), []) - | ERROR (NoData) -> assert false - | ERROR (Data d) -> - (s, (ED.mkApp errorc (RawOpaqueData.of_string d) []), []) - let diagnostic = - { - Conversion.ty = (TyName "diagnostic"); - pp_doc = - (fun fmt -> - fun () -> - ED.BuiltInPredicate.ADT.document_adt - "Used in builtin variants that return Coq's error rather than failing" - (let open Conversion in TyName "diagnostic") - [("ok", "Success", ["diagnostic"]); - ("error", "Failure", ["string"; "diagnostic"])] fmt ()); - pp = - (fun fmt -> - function - | OK -> Format.fprintf fmt "OK" - | ERROR (NoData) -> Format.fprintf fmt "ERROR _" - | ERROR (Data s) -> Format.fprintf fmt "ERROR %S" s); - embed = embed_diagnostic; - readback = readback_diagnostic - } - end -module AlgebraicData = - struct - include ED.BuiltInPredicate.ADT - type name = string - type doc = string - let declare x = - let module R = (val !r) in - ED.BuiltInPredicate.ADT.adt ~look:R.deref_head - ~mkinterval:R.mkinterval ~mkConst:R.mkConst - ~alloc:FlexibleData.Elpi.make ~mkUnifVar:RawData.mkUnifVar x - end -module BuiltInPredicate = - struct - include ED.BuiltInPredicate - exception No_clause = ED.No_clause - let mkData x = Data x - let ioarg a = - let open Conversion in - { - a with - pp = - (fun fmt -> - function - | Data x -> a.pp fmt x - | NoData -> Format.fprintf fmt "_"); - embed = - (fun ~depth -> - fun hyps -> - fun csts -> - fun state -> - function - | Data x -> a.embed ~depth hyps csts state x - | NoData -> assert false); - readback = - (fun ~depth -> - fun hyps -> - fun csts -> - fun state -> - fun t -> - let module R = (val !r) in - let open R in - match R.deref_head ~depth t with - | ED.Term.Arg _|ED.Term.AppArg _ -> assert false - | ED.Term.UVar _|ED.Term.AppUVar _|ED.Term.Discard - -> (state, NoData, []) - | _ -> - let (state, x, gls) = - a.readback ~depth hyps csts state t in - (state, (mkData x), gls)) - } - let ioarg_any = - let open Conversion in - { - BuiltInData.any with - pp = - (fun fmt -> - function - | Data x -> BuiltInData.any.pp fmt x - | NoData -> Format.fprintf fmt "_"); - embed = - (fun ~depth -> - fun _ -> - fun _ -> - fun state -> - function - | Data x -> (state, x, []) - | NoData -> assert false); - readback = - (fun ~depth -> - fun _ -> - fun _ -> - fun state -> - fun t -> - let module R = (val !r) in - match R.deref_head ~depth t with - | ED.Term.Discard -> (state, NoData, []) - | _ -> (state, (Data t), [])) - } - module Notation = - struct - let (!:) x = ((), (Some x)) - let (+!) a b = (a, (Some b)) - let (?:) x = ((), x) - let (+?) a b = (a, b) - end - end -module Query = - struct - type name = string - type ('f, 'c) arguments = ('f, 'c) ED.Query.arguments = - | N: (unit, 'c) arguments - | D: ('a, #Conversion.ctx as 'c) Conversion.t * 'a * ('x, 'c) arguments - -> ('x, 'c) arguments - | Q: ('a, #Conversion.ctx as 'c) Conversion.t * name * ('x, 'c) - arguments -> (('a * 'x), 'c) arguments - type 'c obj_builder = Data.state -> 'c constraint 'c = #Conversion.ctx - type _ t = - | Query: ('a, 'x, 'c) query_contents * ('a, 'k, Conversion.ctx) - Conversion.context * 'c obj_builder -> 'x t - and ('a, 'x, 'c) query_contents = - { - context: 'a list ; - predicate: string ; - arguments: ('x, 'c) arguments } - let compile (state, p) loc (Query - ({ predicate; arguments; context }, cc, obj)) = - let (state, predicate) = - Compiler.Symbols.allocate_global_symbol_str state predicate in - let q = - let open ED.Query in - Query ({ predicate; arguments; context }, cc, obj) in - Compiler.query_of_data state p loc q - end -module State = - struct - include ED.State - let declare ~name ~pp ~init = - declare ~name ~pp ~init ~clause_compilation_is_over:(fun x -> x) - ~goal_compilation_is_over:(fun ~args:_ -> fun x -> Some x) - ~compilation_is_over:(fun x -> Some x) - ~execution_is_over:(fun x -> Some x) - end -module RawQuery = - struct - let mk_Arg = Compiler.mk_Arg - let is_Arg = Compiler.is_Arg - type 'a query_readback = - Data.term Data.StrMap.t -> Data.constraints -> State.t -> 'a - let compile (state, p) f = Compiler.query_of_term state p f - end -module Quotation = - struct - include Compiler - let declare_backtick ~name f = - Compiler.CustomFunctorCompilation.declare_backtick_compilation name - (fun s -> fun x -> f s (EA.Func.show x)) - let declare_singlequote ~name f = - Compiler.CustomFunctorCompilation.declare_singlequote_compilation name - (fun s -> fun x -> f s (EA.Func.show x)) - let term_at ~depth s x = Compiler.term_of_ast ~depth s x - let quote_syntax_runtime s q = - let module R = (val !r) in - Compiler.quote_syntax (`Runtime R.mkConst) s q - let quote_syntax_compiletime s q = - let (s, l, t) = Compiler.quote_syntax `Compiletime s q in (s, l, t) - end -module Utils = - struct - let lp_list_to_list ~depth t = - let module R = (val !r) in let open R in lp_list_to_list ~depth t - let list_to_lp_list tl = - let module R = (val !r) in let open R in list_to_lp_list tl - let get_assignment = - function - | Elpi.Arg _ -> assert false - | Elpi.Ref { ED.contents = t } -> - let module R = (val !r) in if t == ED.dummy then None else Some t - let move ~from ~to_ t = - let module R = (val !r) in - let open R in R.hmove ~from ~to_ ?avoid:None t - let beta ~depth t args = - let module R = (val !r) in - let open R in R.deref_appuv ~from:depth ~to_:depth ?avoid:None args t - let error = Util.error - let type_error = Util.type_error - let anomaly = Util.anomaly - let warn = Util.warn - let printf = Util.printf - let eprintf = Util.eprintf - let clause_of_term ?name ?graft ~depth loc term = - let open EA in - let module Data = ED.Term in - let module R = (val !r) in - let open R in - let rec aux d ctx t = - match R.deref_head ~depth:d t with - | Data.Const i when (i >= 0) && (i < depth) -> - error "program_of_term: the term is not closed" - | Data.Const i when i < 0 -> Term.mkCon (ED.Constants.show i) - | Data.Const i -> Util.IntMap.find i ctx - | Data.Lam t -> - let s = "x" ^ (string_of_int d) in - let ctx = Util.IntMap.add d (Term.mkCon s) ctx in - Term.mkLam s (aux (d + 1) ctx t) - | Data.App (c, x, xs) -> - let c = aux d ctx (R.mkConst c) in - let x = aux d ctx x in - let xs = List.map (aux d ctx) xs in - Term.mkApp loc (c :: x :: xs) - | Data.Arg _|Data.AppArg _ -> assert false - | Data.Cons (hd, tl) -> - let hd = aux d ctx hd in - let tl = aux d ctx tl in Term.mkSeq [hd; tl] - | Data.Nil -> Term.mkNil - | Data.Builtin (c, xs) -> - let c = aux d ctx (R.mkConst c) in - let xs = List.map (aux d ctx) xs in - Term.mkApp loc (c :: xs) - | Data.CData x -> Term.mkC x - | Data.UVar _|Data.AppUVar _ -> - error "program_of_term: the term contains uvars" - | Data.Discard -> Term.mkCon "_" in - let attributes = - (match name with | Some x -> [Clause.Name x] | None -> []) @ - (match graft with - | Some (`After, x) -> [Clause.After x] - | Some (`Before, x) -> [Clause.Before x] - | None -> []) in - [Program.Clause - { - Clause.loc = loc; - attributes; - body = (aux depth Util.IntMap.empty term) - }] - let map_acc = BuiltInData.map_acc - module type Show = Util.Show - module type Show1 = Util.Show1 - module Map = Util.Map - module Set = Util.Set - end -module RawPp = - struct - let term depth fmt t = - let module R = (val !r) in - let open R in R.Pp.uppterm depth [] 0 ED.empty_env fmt t - let constraints f c = - let module R = (val !r) in - let open R in - Util.pplist ~boxed:true (R.pp_stuck_goal ?pp_ctx:None) "" f c - let list = Util.pplist - module Debug = - struct - let term depth fmt t = - let module R = (val !r) in - let open R in R.Pp.ppterm depth [] 0 ED.empty_env fmt t - let show_term = ED.show_term - end - end -module PPX = - struct - module Doc = - struct - let comment = ED.BuiltInPredicate.pp_comment - let kind fmt ty ~doc = - ED.BuiltInPredicate.ADT.document_kind fmt ty doc - let constructor fmt ~name ~doc ~ty ~args = - ED.BuiltInPredicate.ADT.document_constructor fmt name doc - (List.map ED.Conversion.show_ty_ast (args @ [ty])) - let adt ~doc ~ty ~args = - ED.BuiltInPredicate.ADT.document_adt doc ty - (List.map - (fun (n, s, a) -> - (n, s, (List.map ED.Conversion.show_ty_ast (a @ [ty])))) - args) - let show_ty_ast = ED.Conversion.show_ty_ast - end - let readback_int ~depth _ c s x = - BuiltInData.int.Conversion.readback ~depth ((new Conversion.ctx) []) c - s x - let readback_float ~depth _ c s x = - BuiltInData.float.Conversion.readback ~depth ((new Conversion.ctx) []) - c s x - let readback_string ~depth _ c s x = - BuiltInData.string.Conversion.readback ~depth ((new Conversion.ctx) []) - c s x - let readback_list = BuiltInData.readback_list - let readback_loc ~depth _ c s x = - BuiltInData.loc.Conversion.readback ~depth ((new Conversion.ctx) []) c - s x - let readback_nominal ~depth _ c s x = - BuiltInData.nominal.Conversion.readback ~depth - ((new Conversion.ctx) []) c s x - let embed_int ~depth _ c s x = - BuiltInData.int.Conversion.embed ~depth ((new Conversion.ctx) []) c s x - let embed_float ~depth _ c s x = - BuiltInData.float.Conversion.embed ~depth ((new Conversion.ctx) []) c s - x - let embed_string ~depth _ c s x = - BuiltInData.string.Conversion.embed ~depth ((new Conversion.ctx) []) c - s x - let embed_list = BuiltInData.embed_list - let embed_loc ~depth _ c s x = - BuiltInData.loc.Conversion.embed ~depth ((new Conversion.ctx) []) c s x - let embed_nominal ~depth _ c s x = - BuiltInData.nominal.Conversion.embed ~depth ((new Conversion.ctx) []) c - s x - type context_description = - | C: ('a, 'k, 'c) Conversion.context -> context_description - let readback_context - { Conversion.conv = conv; to_key; push; is_entry_for_nominal; init } - ctx ~depth hyps constraints state = - let module CMap = RawData.Constants.Map in - let filtered_hyps = - List.fold_left - (fun m -> - fun hyp -> - match is_entry_for_nominal hyp with - | None -> m - | Some idx -> - (if CMap.mem idx m - then - Utils.type_error - "more than one context entry for the same nominal"; - CMap.add idx hyp m)) CMap.empty hyps in - let rec aux state gls i = - if i = depth - then (state, (List.concat (List.rev gls))) - else - if not (CMap.mem i filtered_hyps) - then aux state gls (i + 1) - else - (let hyp = CMap.find i filtered_hyps in - let hyp_depth = hyp.Data.hdepth in - let (state, (nominal, t), gls_t) = - conv.Conversion.readback ~depth:hyp_depth ctx constraints - state hyp.Data.hsrc in - assert (nominal = i); - (let s = to_key ~depth:hyp_depth t in - let state = - push ~depth:i state s - { Conversion.entry = t; depth = hyp_depth } in - aux state (gls_t :: gls) (i + 1))) in - let state = init state in aux state [] 0 - end - diff --git a/src/.ppcache/API.mli b/src/.ppcache/API.mli deleted file mode 100644 index 78d96292d..000000000 --- a/src/.ppcache/API.mli +++ /dev/null @@ -1,724 +0,0 @@ -(*17cbedc324e731e950a3163806e4dddda4081e81 *src/API.mli --cookie elpi_trace="false"*) -#1 "src/API.mli" -[@@@ocaml.text " This module is the API for clients of the Elpi library. "] -[@@@ocaml.text - " These APIs are sufficient to parse programs and queries from text, run\n the interpreter and finally print the result "] -module Ast : -sig - type program - type query - module Loc : - sig - type t = - { - source_name: string ; - source_start: int ; - source_stop: int ; - line: int ; - line_starts_at: int } - val pp : Format.formatter -> t -> unit - val show : t -> string - val equal : t -> t -> bool - val compare : t -> t -> int - val initial : string -> t - end -end -module Setup : -sig - type builtins - type elpi - val init : - builtins:builtins list -> - basedir:string -> string list -> (elpi * string list)[@@ocaml.doc - " Initialize ELPI.\n [init] must be called before invoking the parser.\n [builtins] the set of built-in predicates, eg [Elpi_builtin.std_builtins]\n [basedir] current working directory (used to make paths absolute);\n [argv] is list of options, see the {!val:usage} string;\n It returns part of [argv] not relevant to ELPI and a handle [elpi]\n to an elpi instance equipped with the given builtins. "] - val usage : string[@@ocaml.doc " Usage string "] - val trace : string list -> unit[@@ocaml.doc - " Set tracing options.\n [trace argv] can be called before {!module:Execute}.\n [argv] is expected to only contain options relevant for\n the tracing facility. "] - val set_warn : (?loc:Ast.Loc.t -> string -> unit) -> unit[@@ocaml.doc - " Override default runtime error functions (they call exit) "] - val set_error : (?loc:Ast.Loc.t -> string -> 'a) -> unit - val set_anomaly : (?loc:Ast.Loc.t -> string -> 'a) -> unit - val set_type_error : (?loc:Ast.Loc.t -> string -> 'a) -> unit - val set_std_formatter : Format.formatter -> unit - val set_err_formatter : Format.formatter -> unit -end -module Parse : -sig - val program : - elpi:Setup.elpi -> - ?print_accumulated_files:bool -> string list -> Ast.program[@@ocaml.doc - " [program file_list] parses a list of files "] - val program_from_stream : - elpi:Setup.elpi -> - ?print_accumulated_files:bool -> - Ast.Loc.t -> char Stream.t -> Ast.program - val goal : Ast.Loc.t -> string -> Ast.query[@@ocaml.doc - " [goal file_list] parses the query "] - val goal_from_stream : Ast.Loc.t -> char Stream.t -> Ast.query - exception ParseError of Ast.Loc.t * string -end -module Data : -sig - module StrMap : - sig - include Map.S with type key = string - val show : (Format.formatter -> 'a -> unit) -> 'a t -> string - val pp : - (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit - end - type term - type constraints - type state - type pretty_printer_context - type 'a solution = - { - assignments: term StrMap.t ; - constraints: constraints ; - state: state ; - output: 'a ; - pp_ctx: pretty_printer_context } - type hyp = { - hdepth: int ; - hsrc: term } - type hyps = hyp list - type constant = int - module Constants : - sig - module Map : - sig - include Map.S with type key = constant - val show : (Format.formatter -> 'a -> unit) -> 'a t -> string - val pp : - (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit - end - end -end -module Compile : -sig - module StrSet : - sig - include Set.S with type elt = string - val show : t -> string - val pp : Format.formatter -> t -> unit - end - type flags = { - defined_variables: StrSet.t ; - print_passes: bool } - val default_flags : flags - type program - type 'a query - type 'a executable - exception CompileError of Ast.Loc.t option * string - val program : flags:flags -> elpi:Setup.elpi -> Ast.program list -> program - type compilation_unit - val unit : - elpi:Setup.elpi -> flags:flags -> Ast.program -> compilation_unit - val assemble : elpi:Setup.elpi -> compilation_unit list -> program - val query : program -> Ast.query -> unit query - val optimize : 'a query -> 'a executable - val static_check : checker:program -> 'a query -> bool[@@ocaml.doc - " Runs a checker. Returns true if no errors were found.\n See also Builtins.default_checker. "] -end -module Execute : -sig - type 'a outcome = - | Success of 'a Data.solution - | Failure - | NoMoreSteps - val once : - ?max_steps:int -> - ?delay_outside_fragment:bool -> 'a Compile.executable -> 'a outcome - val loop : - ?delay_outside_fragment:bool -> - 'a Compile.executable -> - more:(unit -> bool) -> pp:(float -> 'a outcome -> unit) -> unit - [@@ocaml.doc - " Prolog's REPL.\n [pp] is called on all solutions.\n [more] is called to know if another solution has to be searched for. "] -end -module Pp : -sig - val term : - Data.pretty_printer_context -> Format.formatter -> Data.term -> unit - val constraints : - Data.pretty_printer_context -> - Format.formatter -> Data.constraints -> unit - val state : Format.formatter -> Data.state -> unit - val query : Format.formatter -> 'a Compile.query -> unit - module Ast : sig val program : Format.formatter -> Ast.program -> unit end -end -[@@@ocaml.text - " This API lets one exchange with the host application opaque (primitive)\n data such as integers or strings as well as algebraic data such OCaml's\n ADS. No support for binders or unification variables at thil point. "] -module Conversion : -sig - type ty_ast = - | TyName of string - | TyApp of string * ty_ast * ty_ast list - type extra_goals = Data.term list - exception TypeErr of ty_ast * int * Data.term - class ctx : Data.hyps -> object method raw : Data.hyps end - type ('a, 'c) embedding = - depth:int -> - 'c -> - Data.constraints -> - Data.state -> 'a -> (Data.state * Data.term * extra_goals) - constraint - 'c = - #ctx - type ('a, 'c) readback = - depth:int -> - 'c -> - Data.constraints -> - Data.state -> Data.term -> (Data.state * 'a * extra_goals) - constraint - 'c = - #ctx - type ('a, 'c) t = - { - ty: ty_ast ; - pp_doc: Format.formatter -> unit -> unit ; - pp: Format.formatter -> 'a -> unit ; - embed: ('a, 'c) embedding ; - readback: ('a, 'c) readback } constraint 'c = #ctx - val (^^) : ('a, ctx) t -> ('a, 'c) t - type 'a ctx_entry = { - entry: 'a ; - depth: int } - val pp_ctx_entry : - (Format.formatter -> 'a -> unit) -> - Format.formatter -> 'a ctx_entry -> unit - val show_ctx_entry : - (Format.formatter -> 'a -> unit) -> 'a ctx_entry -> string - type 'a ctx_field = 'a ctx_entry Data.Constants.Map.t - type ('a, 'k, 'c) context = - { - is_entry_for_nominal: Data.hyp -> Data.constant option ; - to_key: depth:int -> 'a -> 'k ; - push: depth:int -> Data.state -> 'k -> 'a ctx_entry -> Data.state ; - pop: depth:int -> Data.state -> 'k -> Data.state ; - conv: ((Data.constant * 'a), #ctx as 'c) t ; - init: Data.state -> Data.state ; - get: Data.state -> 'a ctx_field } - type 'c ctx_readback = - depth:int -> - Data.hyps -> - Data.constraints -> Data.state -> (Data.state * 'c * extra_goals) - constraint 'c = #ctx - type dummy - val in_raw_ctx : ctx ctx_readback - val in_raw : (dummy, dummy, #ctx as 'a) context -end[@@ocaml.doc - " This module defines what embedding and readback functions are "] -module OpaqueData : -sig - type doc = string - type name = string - type 'a declaration = - { - name: name ; - cname: name ; - doc: doc ; - pp: Format.formatter -> 'a -> unit ; - compare: 'a -> 'a -> int ; - hash: 'a -> int ; - hconsed: bool ; - constants: (name * 'a) list }[@@ocaml.doc - " The [eq] function is used by unification. Limitation: unification of\n * two cdata cannot alter the constraint store. This can be lifted in the\n * future if there is user request.\n *\n * If the hconsed is true, then the [readback] function is\n * automatically hashcons the data using the [eq] and [hash] functions.\n "] - type 'a cdata_with_constants - val declare : 'a declaration -> 'a cdata_with_constants - val build_conversion : 'a cdata_with_constants -> ('a, 'c) Conversion.t - val embed : 'a cdata_with_constants -> ('a, 'c) Conversion.embedding - val readback : 'a cdata_with_constants -> ('a, 'c) Conversion.readback - val rest : - 'a cdata_with_constants -> - (Conversion.ty_ast * (Format.formatter -> 'a -> unit) * - (Format.formatter -> unit -> unit)) -end[@@ocaml.doc - " Declare data from the host application that is opaque (no syntax), like\n int but not like list or pair "] -module AlgebraicData : -sig - type name = string - type doc = string - type ('match_stateful_t, 'match_t, 't) match_t = - | M of (ok:'match_t -> ko:(unit -> Data.term) -> 't -> Data.term) - | MS of - (ok:'match_stateful_t -> - ko:(Data.state -> (Data.state * Data.term * Conversion.extra_goals)) - -> - 't -> - Data.state -> (Data.state * Data.term * Conversion.extra_goals)) - - type ('build_stateful_t, 'build_t) build_t = - | B of 'build_t - | BS of 'build_stateful_t - type ('stateful_builder, 'builder, 'stateful_matcher, 'matcher, 'self, - 'c) constructor_arguments = - | N: (Data.state -> (Data.state * 'self), 'self, - Data.state -> (Data.state * Data.term * Conversion.extra_goals), - Data.term, 'self, 'c) constructor_arguments - | A: ('a, 'c) Conversion.t * ('bs, 'b, 'ms, 'm, 'self, 'c) - constructor_arguments -> ('a -> 'bs, 'a -> 'b, 'a -> 'ms, 'a -> 'm, - 'self, 'c) constructor_arguments - | S: ('bs, 'b, 'ms, 'm, 'self, 'c) constructor_arguments -> - ('self -> 'bs, 'self -> 'b, 'self -> 'ms, 'self -> 'm, 'self, 'c) - constructor_arguments - | C: (('self, 'c) Conversion.t -> ('a, 'c) Conversion.t) * ('bs, - 'b, 'ms, 'm, 'self, 'c) constructor_arguments -> ('a -> 'bs, 'a -> 'b, - 'a -> 'ms, 'a -> 'm, 'self, 'c) constructor_arguments [@@ocaml.doc - " GADT for describing the type of the constructor:\n - N is the terminator\n - A(a,...) is an argument of type a (a is a Conversion.t)\n - S stands for self\n - C stands for container\n "] - type ('t, 'c) constructor = - | K: name * doc * ('build_stateful_t, 'build_t, 'match_stateful_t, - 'match_t, 't, 'c) constructor_arguments * ('build_stateful_t, 'build_t) - build_t * ('match_stateful_t, 'match_t, 't) match_t -> ('t, 'c) - constructor - type ('t, 'c) declaration = - { - ty: Conversion.ty_ast ; - doc: doc ; - pp: Format.formatter -> 't -> unit ; - constructors: ('t, 'c) constructor list } constraint 'c = #Conversion.ctx - val declare : ('t, 'c) declaration -> ('t, 'c) Conversion.t -end[@@ocaml.doc - " Declare data from the host application that has syntax, like\n list or pair but not like int. So far there is no support for\n data with binder using this API. The type of each constructor is\n described using a GADT so that the code to build or match the data\n can be given the right type. Example: define the ADT for \"option a\"\n{[\n let option_declaration a = {\n ty = TyApp(\"option\",a.ty,[]);\n doc = \"The option type (aka Maybe)\";\n pp = (fun fmt -> function\n | None -> Format.fprintf fmt \"None\"\n | Some x -> Format.fprintf fmt \"Some %a\" a.pp x);\n constructors = [\n K(\"none\",\"nothing in this case\",\n N, (* no arguments *)\n B None, (* builder *)\n M (fun ~ok ~ko -> function None -> ok | _ -> ko ())); (* matcher *)\n K(\"some\",\"something in this case\",\n A (a,N), (* one argument of type a *)\n B (fun x -> Some x), (* builder *)\n M (fun ~ok ~ko -> function Some x -> ok x | _ -> ko ())); (* matcher *)\n ]\n }\n\n ]}\n\n [K] stands for \"constructor\", [B] for \"build\", [M] for \"match\".\n Variants [BS] and [MS] give read/write access to the state.\n\n"] -module BuiltInPredicate : -sig - exception No_clause - type name = string - type doc = string - type 'a oarg = - | Keep - | Discard - type 'a ioarg = private - | Data of 'a - | NoData - type ('function_type, 'inernal_outtype_in, 'internal_hyps) ffi = - | In: ('t, 'h) Conversion.t * doc * ('i, 'o, 'h) ffi -> ('t -> 'i, - 'o, 'h) ffi - | Out: ('t, 'h) Conversion.t * doc * ('i, ('o * 't option), 'h) ffi -> - ('t oarg -> 'i, 'o, 'h) ffi - | InOut: ('t ioarg, 'h) Conversion.t * doc * ('i, ('o * 't option), - 'h) ffi -> ('t ioarg -> 'i, 'o, 'h) ffi - | Easy: doc -> (depth:int -> 'o, 'o, 'h) ffi - | Read: doc -> (depth:int -> 'h -> Data.constraints -> Data.state -> 'o, - 'o, 'h) ffi - | Full: doc -> - (depth:int -> - 'h -> - Data.constraints -> - Data.state -> (Data.state * 'o * Conversion.extra_goals), - 'o, 'h) ffi - | VariadicIn: ('t, 'h) Conversion.t * doc -> - ('t list -> - depth:int -> 'h -> Data.constraints -> Data.state -> (Data.state * 'o), - 'o, 'h) ffi - | VariadicOut: ('t, 'h) Conversion.t * doc -> - ('t oarg list -> - depth:int -> - 'h -> - Data.constraints -> - Data.state -> (Data.state * ('o * 't option list option)), - 'o, 'h) ffi - | VariadicInOut: ('t ioarg, 'h) Conversion.t * doc -> - ('t ioarg list -> - depth:int -> - 'h -> - Data.constraints -> - Data.state -> (Data.state * ('o * 't option list option)), - 'o, 'h) ffi - type t = - | Pred: name * ('a, unit, 'h) ffi * 'h Conversion.ctx_readback * 'a -> t - val mkData : 'a -> 'a ioarg[@@ocaml.doc - " Tools for InOut arguments.\n *\n * InOut arguments need to be equipped with an 'a ioarg Conversion.t.\n * The ioarg adaptor here maps variables to NoData and anything else to the\n * to Data of the provided 'a Conversion.t.\n *\n * If the 'a is an atomic data type, eg int, then things are good.\n * If the 'a is an algebraic data type then some more work has to be done\n * in order to have a good implementation, but the type system cannot\n * enforce it hence this documentation. Let's take the example of int option.\n * The Conversion.t to be passed is [int ioarg option ioarg Conversion.t],\n * that is, ioarg should wrap each type constructor. In this way the user\n * can pass non-ground terms. Eg\n * given term : X none some X some 3\n * readback to: NoData Data None Data (Some NoData) Data (Some (Data 3))\n *\n * Alternatively the data type 'a must be able to represent unification\n * variables, such as the raw terms, see [ioarg_any] below.\n *\n * An example of an API taking advantage of this feature is\n * pred typecheck i:term, o:ty, o:diagnostic\n * that can be used to both check a term is well typed and backtrack if not\n * typecheck T TY ok\n * or assert a term is illtyped or to test weather it is illtyped\n * typecheck T TY (error _), typecheck T TY Diagnostic\n * The ML code can see in which case we are and for example optimize the\n * first case by not even generating the error message (since error \"message\"\n * would fail to unify with ok anyway) or the second one by not assigning TY.\n "] - val ioarg : ('t, 'c) Conversion.t -> ('t ioarg, 'c) Conversion.t - val ioarg_any : (Data.term ioarg, 'c) Conversion.t - module Notation : - sig - val (?:) : 'a -> (unit * 'a) - val (!:) : 'a -> (unit * 'a option) - val (+?) : 'a -> 'b -> ('a * 'b) - val (+!) : 'a -> 'b -> ('a * 'b option) - end -end -module BuiltIn : -sig - type doc_spec = - | DocAbove - | DocNext [@@ocaml.doc - " Where to print the documentation. For the running example DocAbove\n * generates\n * % [div N M D R] division of N by M gives D with reminder R\n * pred div i:int, i:int, o:int, o:int.\n * while DocNext generates\n * pred div % division of N by M gives D with reminder R\n * i:int, % N\n * i:int, % M\n * o:int, % D\n * o:int. % R\n * The latter format it is useful to give longer doc for each argument. "] - type declaration = - | MLCode of BuiltInPredicate.t * doc_spec - | MLData: ('a, 'c) Conversion.t -> declaration - | LPDoc of string - | LPCode of string - val declare : file_name:string -> declaration list -> Setup.builtins - [@@ocaml.doc " What is passed to [Setup.init] "] - val document_fmt : Format.formatter -> Setup.builtins -> unit[@@ocaml.doc - " Prints in LP syntax the \"external\" declarations.\n * The file builtin.elpi is generated by calling this API on the\n * declaration list from elpi_builtin.ml "] - val document_file : ?header:string -> Setup.builtins -> unit -end[@@ocaml.doc - " Setup.init takes a list of declarations of data types and predicates,\n plus some doc and eventually some Elpi code. All this constitutes the\n \"prelude\", that is what is avaiable to an Elpi program "] -module Query : -sig - type name = string - type (_, _) arguments = - | N: (unit, 'c) arguments - | D: ('a, #Conversion.ctx as 'c) Conversion.t * 'a * ('x, 'c) arguments - -> ('x, 'c) arguments - | Q: ('a, #Conversion.ctx as 'c) Conversion.t * name * ('x, 'c) arguments - -> (('a * 'x), 'c) arguments - type 'c obj_builder = Data.state -> 'c constraint 'c = #Conversion.ctx - type _ t = - | Query: ('a, 'x, 'c) query_contents * ('a, 'k, Conversion.ctx) - Conversion.context * 'c obj_builder -> 'x t - and ('a, 'x, 'c) query_contents = - { - context: 'a list ; - predicate: string ; - arguments: ('x, 'c) arguments } - val compile : Compile.program -> Ast.Loc.t -> 'a t -> 'a Compile.query -end[@@ocaml.doc - " Commodity module to build a simple query\n and extract the output from the solution found by Elpi.\n\n Example: \"foo data Output\" where [data] has type [t] ([a] is [t Conversion.t])\n and [Output] has type [v] ([b] is a [v Conversion.t]) can be described as:\n{[\n\n let q : (v * unit) t = Query {\n predicate = \"foo\";\n arguments = D(a, data,\n Q(b, \"Output\",\n N))\n }\n\n ]}\n\n Then [compile q] can be used to obtain the compiled query such that the\n resulting solution has a fied output of type [(v * unit)]. Example:\n{[\n\n Query.compile q |> Compile.link |> Execute.once |> function\n | Execute.Success { output } -> output\n | _ -> ...\n\n ]} "] -[@@@ocaml.text - " This API lets one access the low lever representation of terms in order\n to exchange data with binders and unification variables with the host\n application. It also lets one define quotations and extend the state\n theraded by Elpi with custom data. "] -module State : -sig - type 'a component[@@ocaml.doc - " 'a MUST be purely functional, i.e. backtracking is implemented by using\n * an old binding for 'a.\n * This limitation can be lifted if there is user request. "] - val declare : - name:string -> - pp:(Format.formatter -> 'a -> unit) -> - init:(unit -> 'a) -> 'a component - type t = Data.state - val get : 'a component -> t -> 'a - val set : 'a component -> t -> 'a -> t - val update : 'a component -> t -> ('a -> 'a) -> t[@@ocaml.doc - " Allowed to raise BuiltInPredicate.No_clause "] - val update_return : 'a component -> t -> ('a -> ('a * 'b)) -> (t * 'b) -end[@@ocaml.doc - " State is a collection of purely functional piece of data carried\n by the interpreter. Such data is kept in sync with the backtracking, i.e.\n changes made in a branch are lost if that branch fails.\n It can be used to both store custom constraints to be manipulated by\n custom solvers, or any other piece of data the host application may\n need to use. "] -module FlexibleData : -sig - module Elpi : - sig - type t - val make : ?name:string -> Data.state -> (Data.state * t) - val get : name:string -> Data.state -> t option - val pp : Format.formatter -> t -> unit - val show : t -> string - val equal : t -> t -> bool - end[@@ocaml.doc " key for Elpi's flexible data "] - module type Host = - sig - type t - val compare : t -> t -> int - val pp : Format.formatter -> t -> unit - val show : t -> string - end - module Map : - functor (Host : Host) -> - sig - type t - val empty : t - val add : Elpi.t -> Host.t -> t -> t - val remove_elpi : Elpi.t -> t -> t - val remove_host : Host.t -> t -> t - val filter : (Host.t -> Elpi.t -> bool) -> t -> t - val fold : - (Host.t -> Elpi.t -> Data.term option -> 'a -> 'a) -> t -> 'a -> 'a - val elpi : Host.t -> t -> Elpi.t - val host : Elpi.t -> t -> Host.t - val uvmap : t State.component - val pp : Format.formatter -> t -> unit - val show : t -> string - end - [@@@ocaml.text - " Example from Hol-light + elpi:\n{[\n\n module UV2STV = FlexibleData.Map(struct\n type t = int\n let compare x y = x - y\n let pp fmt i = Format.fprintf fmt \"%d\" i\n let show = string_of_int\n end)\n\n let stv = ref 0\n let incr_get r = incr r; !r\n\n let record k state =\n State.update_return UV2STV.uvmap state (fun m ->\n try m, Stv (UV2STV.host k m)\n with Not_found ->\n let j = incr_get stv in\n UV2STV.add k j m, Stv j)\n\n (* The constructor name \"uvar\" is special and has to be used with the\n following Conversion.t *)\n\n let hol_pretype = AlgebraicData.declare {\n ty = TyName \"pretype\";\n doc = \"The algebraic data type of pretypes\";\n pp = (fun fmt t -> ...);\n constructors = [\n ...\n K(\"uvar\",\"\",A(uvar,N),\n BS (fun (k,_) state -> record k state),\n M (fun ~ok ~ko _ -> ko ()))\n ]\n }\n\n ]}\n\n In this way an Elpi term containig a variable [X] twice gets read back\n using [Stv i] for the same [i].\n\n "] - val uvar : ((Elpi.t * Data.term list), 'c) Conversion.t -end[@@ocaml.doc - " Flexible data is for unification variables. One can use Elpi's unification\n variables to represent the host equivalent, here the API the keep a link\n between the two. "] -module BuiltInData : -sig - val int : (int, 'c) Conversion.t[@@ocaml.doc - " See Elpi_builtin for a few more "] - val float : (float, 'c) Conversion.t - val string : (string, 'c) Conversion.t - val list : ('a, 'c) Conversion.t -> ('a list, 'c) Conversion.t - val loc : (Ast.Loc.t, 'c) Conversion.t - val bool : (bool, 'c) Conversion.t - val char : (char, 'c) Conversion.t - val in_stream : ((in_channel * string), 'c) Conversion.t - val out_stream : ((out_channel * string), 'c) Conversion.t - type diagnostic = private - | OK - | ERROR of string BuiltInPredicate.ioarg - val diagnostic : (diagnostic, 'c) Conversion.t - val mkOK : diagnostic - val mkERROR : string -> diagnostic - val poly : string -> (Data.term, 'c) Conversion.t - val closed : string -> ((Data.term * int), 'c) Conversion.t - val any : (Data.term, 'c) Conversion.t - val nominal : (Data.constant, 'c) Conversion.t -end[@@ocaml.doc " Conversion for Elpi's built-in data types "] -module Utils : -sig - val error : ?loc:Ast.Loc.t -> string -> 'a[@@ocaml.doc - " A regular error (fatal) "] - val anomaly : ?loc:Ast.Loc.t -> string -> 'a[@@ocaml.doc - " An invariant is broken, i.e. a bug "] - val type_error : ?loc:Ast.Loc.t -> string -> 'a[@@ocaml.doc - " A type error (in principle ruled out by [elpi-checker.elpi]) "] - val warn : ?loc:Ast.Loc.t -> string -> unit[@@ocaml.doc - " A non fatal warning "] - val printf : ('a, Format.formatter, unit) format -> 'a[@@ocaml.doc - " alias for printf and eprintf that write on the formatters set in Setup "] - val eprintf : ('a, Format.formatter, unit) format -> 'a - val list_to_lp_list : Data.term list -> Data.term[@@ocaml.doc - " link between OCaml and LP lists. Note that [1,2|X] is not a valid\n * OCaml list! "] - val lp_list_to_list : depth:int -> Data.term -> Data.term list - val get_assignment : FlexibleData.Elpi.t -> Data.term option[@@ocaml.doc - " The body of an assignment, if any (LOW LEVEL).\n * Use [look] and forget about this API since the term you get\n * needs to be moved and/or reduced, and you have no API for this. "] - val clause_of_term : - ?name:string -> - ?graft:([ `After | `Before ] * string) -> - depth:int -> Ast.Loc.t -> Data.term -> Ast.program[@@ocaml.doc - " Hackish, in particular the output should be a compiled program "] - val move : from:int -> to_:int -> Data.term -> Data.term[@@ocaml.doc - " Lifting/restriction/beta (LOW LEVEL, don't use) "] - val beta : depth:int -> Data.term -> Data.term list -> Data.term - val map_acc : - (Data.state -> 't -> (Data.state * 'a * Conversion.extra_goals)) -> - Data.state -> - 't list -> (Data.state * 'a list * Conversion.extra_goals)[@@ocaml.doc - " readback/embed on lists "] - module type Show = - sig type t val pp : Format.formatter -> t -> unit val show : t -> string - end - module type Show1 = - sig - type 'a t - val pp : - (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit - val show : (Format.formatter -> 'a -> unit) -> 'a t -> string - end - module Map : - sig - module type S = - sig include Map.S include Show1 with type 'a t := 'a t end - module type OrderedType = - sig include Map.OrderedType include Show with type t := t end - module Make : functor (Ord : OrderedType) -> S with type key = Ord.t - end - module Set : - sig - module type S = sig include Set.S include Show with type t := t end - module type OrderedType = - sig include Set.OrderedType include Show with type t := t end - module Make : functor (Ord : OrderedType) -> S with type elt = Ord.t - end -end -module RawOpaqueData : -sig - type t - type 'a cdata = private - { - cin: 'a -> t ; - isc: t -> bool ; - cout: t -> 'a ; - name: string }[@@ocaml.doc - " If the data_hconsed is true, then the [cin] function below will\n automatically hashcons the data using the [eq] and [hash] functions. "] - val cdata : 'a OpaqueData.cdata_with_constants -> 'a cdata - val pp : Format.formatter -> t -> unit - val show : t -> string - val equal : t -> t -> bool - val compare : t -> t -> int - val hash : t -> int - val name : t -> string - val hcons : t -> t - val ty2 : 'a cdata -> t -> t -> bool - val morph1 : 'a cdata -> ('a -> 'a) -> t -> t - val morph2 : 'a cdata -> ('a -> 'a -> 'a) -> t -> t -> t - val map : 'a cdata -> 'b cdata -> ('a -> 'b) -> t -> t - val int : int cdata - val is_int : t -> bool - val to_int : t -> int - val of_int : int -> Data.term - val float : float cdata - val is_float : t -> bool - val to_float : t -> float - val of_float : float -> Data.term - val string : string cdata - val is_string : t -> bool - val to_string : t -> string - val of_string : string -> Data.term - val loc : Ast.Loc.t cdata - val is_loc : t -> bool - val to_loc : t -> Ast.Loc.t - val of_loc : Ast.Loc.t -> Data.term - val char : char cdata - val is_char : t -> bool - val to_char : t -> char - val of_char : char -> Data.term -end[@@ocaml.doc " Low level module for OpaqueData "] -module RawData : -sig - type constant = Data.constant[@@ocaml.doc - " De Bruijn levels (not indexes):\n the distance of the binder from the root.\n Starts at 0 and grows for bound variables;\n global constants have negative values. "] - type builtin[@@ocaml.doc - " De Bruijn levels (not indexes):\n the distance of the binder from the root.\n Starts at 0 and grows for bound variables;\n global constants have negative values. "] - type term = Data.term - type view = private - | Const of constant - | Lam of term - | App of constant * term * term list - | Cons of term * term - | Nil - | Builtin of builtin * term list - | CData of RawOpaqueData.t - | UnifVar of FlexibleData.Elpi.t * term list - val look : depth:int -> term -> view[@@ocaml.doc - " Terms must be inspected after dereferencing their head.\n If the resulting term is UVar then its uvar_body is such that\n get_assignment uvar_body = None "] - val kool : view -> term - val mkBound : constant -> term[@@ocaml.doc " Smart constructors "] - val mkLam : term -> term - val mkCons : term -> term -> term - val mkNil : term - val mkDiscard : term - val mkCData : RawOpaqueData.t -> term - val mkUnifVar : FlexibleData.Elpi.t -> args:term list -> Data.state -> term - val mkGlobal : constant -> term[@@ocaml.doc - " Lower level smart constructors "] - val mkApp : constant -> term -> term list -> term - val mkAppL : constant -> term list -> term - val mkBuiltin : builtin -> term list -> term - val mkConst : constant -> term - val cmp_builtin : builtin -> builtin -> int - type suspended_goal = { - context: Data.hyps ; - goal: (int * term) } - val constraints : Data.constraints -> suspended_goal list - val no_constraints : Data.constraints - module Constants : - sig - val declare_global_symbol : string -> constant - val show : constant -> string - val eqc : constant - val orc : constant - val andc : constant - val rimplc : constant - val pic : constant - val sigmac : constant - val implc : constant - val cutc : constant - val ctypec : constant - val spillc : constant - module Map = Data.Constants.Map - module Set : Utils.Set.S with type elt = constant - end -end[@@ocaml.doc - " This module exposes the low level representation of terms.\n *\n * The data type [term] is opaque and can only be accessed by using the\n * [look] API that exposes a term [view]. The [look] view automatically\n * substitutes assigned unification variables by their value. "] -module RawQuery : -sig - val mk_Arg : - Data.state -> - name:string -> args:Data.term list -> (Data.state * Data.term) - val is_Arg : Data.state -> Data.term -> bool - type 'a query_readback = - Data.term Data.StrMap.t -> Data.constraints -> State.t -> 'a - val compile : - Compile.program -> - (depth:int -> - Data.hyps -> - Data.constraints -> - Data.state -> - (Data.state * (Ast.Loc.t * Data.term) * 'a query_readback)) - -> 'a Compile.query -end[@@ocaml.doc - " This module lets one generate a query by providing a RawData.term directly "] -module Quotation : -sig - type quotation = - depth:int -> - Data.state -> Ast.Loc.t -> string -> (Data.state * Data.term) - val set_default_quotation : quotation -> unit[@@ocaml.doc - " The default quotation [{{code}}] "] - val register_named_quotation : name:string -> quotation -> unit[@@ocaml.doc - " Named quotation [{{:name code}}] "] - val lp : quotation[@@ocaml.doc " The anti-quotation to lambda Prolog "] - val quote_syntax_runtime : - Data.state -> - 'a Compile.query -> (Data.state * Data.term list * Data.term)[@@ocaml.doc - " See elpi-quoted_syntax.elpi (EXPERIMENTAL, used by elpi-checker) "] - val quote_syntax_compiletime : - Data.state -> - 'a Compile.query -> (Data.state * Data.term list * Data.term) - val term_at : - depth:int -> Data.state -> Ast.query -> (Data.state * Data.term)[@@ocaml.doc - " To implement the string_to_term built-in (AVOID, makes little sense\n * if depth is non zero, since bound variables have no name!) "] - [@@@ocaml.text - " Like quotations but for identifiers that begin and end with\n * \"`\" or \"'\", e.g. `this` and 'that'. Useful if the object language\n * needs something that looks like a string but with a custom compilation\n * (e.g. CD.string like but with a case insensitive comparison) "] - val declare_backtick : - name:string -> (Data.state -> string -> (Data.state * Data.term)) -> unit - val declare_singlequote : - name:string -> (Data.state -> string -> (Data.state * Data.term)) -> unit -end -module RawPp : -sig - val term : int -> Format.formatter -> Data.term -> unit[@@ocaml.doc - " If the term is under [depth] binders this is the function that has to be\n * called in order to print the term correct. WARNING: as of today printing\n * an open term (i.e. containing unification variables) in the *wrong* depth\n * can cause the pruning of the unification variable.\n * This behavior shall be cleaned up in the future "] - val constraints : Format.formatter -> Data.constraints -> unit - val list : - ?max:int -> - ?boxed:bool -> - (Format.formatter -> 'a -> unit) -> - ?pplastelem:(Format.formatter -> 'a -> unit) -> - string -> Format.formatter -> 'a list -> unit - module Debug : - sig - val term : int -> Format.formatter -> Data.term -> unit - val show_term : Data.term -> string - end -end -module PPX : -sig - [@@@ocaml.text " Access to internal API to implement elpi.ppx "] - val readback_int : (int, 'c) Conversion.readback - val readback_float : (float, 'c) Conversion.readback - val readback_string : (string, 'c) Conversion.readback - val readback_list : - ('a, 'c) Conversion.readback -> ('a list, 'c) Conversion.readback - val readback_loc : (Ast.Loc.t, 'c) Conversion.readback - val readback_nominal : (RawData.constant, 'c) Conversion.readback - val embed_int : (int, 'c) Conversion.embedding - val embed_float : (float, 'c) Conversion.embedding - val embed_string : (string, 'c) Conversion.embedding - val embed_list : - ('a, 'c) Conversion.embedding -> ('a list, 'c) Conversion.embedding - val embed_loc : (Ast.Loc.t, 'c) Conversion.embedding - val embed_nominal : (RawData.constant, 'c) Conversion.embedding - type context_description = - | C: ('a, 'k, 'c) Conversion.context -> context_description - val readback_context : - ('a, 'k, 'c) Conversion.context -> - 'c -> - depth:int -> - Data.hyps -> - Data.constraints -> - Data.state -> (Data.state * Conversion.extra_goals) - module Doc : - sig - val kind : Format.formatter -> Conversion.ty_ast -> doc:string -> unit - val comment : Format.formatter -> string -> unit - val constructor : - Format.formatter -> - name:string -> - doc:string -> - ty:Conversion.ty_ast -> args:Conversion.ty_ast list -> unit - val adt : - doc:string -> - ty:Conversion.ty_ast -> - args:(string * string * Conversion.ty_ast list) list -> - Format.formatter -> unit -> unit - val show_ty_ast : ?outer:bool -> Conversion.ty_ast -> string - end -end -[@@@ocaml.text "/*"] - diff --git a/src/.ppcache/data.ml b/src/.ppcache/data.ml index 2011450b1..13d70cb62 100644 --- a/src/.ppcache/data.ml +++ b/src/.ppcache/data.ml @@ -1,4 +1,4 @@ -(*d1ab878a9994ecb249bc95701570d498a788a5b4 *src/data.ml *) +(*7f2ba7fa31dccc0775a96d5831ee46cdbb09241c *src/data.ml *) #1 "src/data.ml" module Fmt = Format module F = Ast.Func @@ -1669,8 +1669,10 @@ module BuiltInPredicate = | S: ('bs, 'b, 'ms, 'm, 'self, 'ctx) constructor_arguments -> ('self -> 'bs, 'self -> 'b, 'self -> 'ms, 'self -> 'm, 'self, 'ctx) constructor_arguments - | C: (('self, 'ctx) Conversion.t -> ('a, 'ctx) Conversion.t) * - ('bs, 'b, 'ms, 'm, 'self, 'ctx) constructor_arguments -> + | C: + (('self, Conversion.ctx) Conversion.t -> + ('a, Conversion.ctx) Conversion.t) + * ('bs, 'b, 'ms, 'm, 'self, 'ctx) constructor_arguments -> ('a -> 'bs, 'a -> 'b, 'a -> 'ms, 'a -> 'm, 'self, 'ctx) constructor_arguments type ('t, 'h) constructor = @@ -1704,16 +1706,17 @@ module BuiltInPredicate = ('t, 'h) compiled_constructor Constants.Map.t let buildk ~mkConst kname = function | [] -> mkConst kname | x::xs -> mkApp kname x xs - let rec readback_args : type a m t h. + let rec readback_args : type a m t. look:(depth:int -> term -> term) -> Conversion.ty_ast -> depth:int -> - h -> + #Conversion.ctx -> constraints -> State.t -> extra_goals list -> term -> - (a, m, t, h) compiled_constructor_arguments -> + (a, m, t, Conversion.ctx) + compiled_constructor_arguments -> a -> term list -> (State.t * t * extra_goals) = fun ~look -> @@ -1743,15 +1746,15 @@ module BuiltInPredicate = readback_args ~look ty ~depth hyps constraints state (gls :: extra) origin rest (convert x) xs - and readback : type t h. + and readback : type t. mkinterval:(int -> int -> int -> term list) -> look:(depth:int -> term -> term) -> alloc:(?name:string -> State.t -> (State.t * 'uk)) -> mkUnifVar:('uk -> args:term list -> State.t -> term) -> Conversion.ty_ast -> - (t, h) compiled_adt -> + (t, Conversion.ctx) compiled_adt -> depth:int -> - h -> + #Conversion.ctx -> constraints -> State.t -> term -> (State.t * t * extra_goals) = @@ -1801,15 +1804,16 @@ module BuiltInPredicate = with | Not_found -> raise (Conversion.TypeErr (ty, depth, t)) - and adt_embed_args : type m a t h. + and adt_embed_args : type m a t. mkConst:(int -> term) -> Conversion.ty_ast -> - (t, h) compiled_adt -> + (t, Conversion.ctx) compiled_adt -> constant -> depth:int -> - h -> + #Conversion.ctx -> constraints -> - (a, m, t, h) compiled_constructor_arguments -> + (a, m, t, Conversion.ctx) + compiled_constructor_arguments -> (State.t -> (State.t * term * extra_goals)) list -> m = @@ -1841,13 +1845,13 @@ module BuiltInPredicate = ((fun state -> d.embed ~depth hyps constraints state x) :: acc)) - and embed : type a h. + and embed : type a. mkConst:(int -> term) -> Conversion.ty_ast -> (Format.formatter -> a -> unit) -> - (a, h) compiled_adt -> + (a, Conversion.ctx) compiled_adt -> depth:int -> - h -> + #Conversion.ctx -> constraints -> State.t -> a -> (State.t * term * extra_goals) = @@ -1875,9 +1879,9 @@ module BuiltInPredicate = matcher ~ok ~ko:(aux rest) t state in aux bindings state let rec compile_arguments : type b bs m ms t. - (bs, b, ms, m, t, 'h) constructor_arguments -> - (t, #Conversion.ctx as 'h) Conversion.t -> - (bs, ms, t, 'h) compiled_constructor_arguments + (bs, b, ms, m, t, Conversion.ctx) constructor_arguments -> + (t, #Conversion.ctx) Conversion.t -> + (bs, ms, t, Conversion.ctx) compiled_constructor_arguments = fun arg -> fun self -> diff --git a/src/API.ml b/src/API.ml index 4d20c8055..f4fc578e0 100644 --- a/src/API.ml +++ b/src/API.ml @@ -260,28 +260,24 @@ module OpaqueData = struct with Not_found -> raise (Conversion.TypeErr(Conversion.TyName name,depth,t)) end | t -> raise (Conversion.TypeErr(Conversion.TyName name,depth,t)) + let declare_cdata cdata name doc constants = + let cd_w_consts = + cdata, name, + List.fold_right (fun (n,v) -> + ED.Constants.Map.add (ED.Global_symbols.declare_global_symbol n) (n,v)) + constants ED.Constants.Map.empty, doc in + let ty, pp, pp_doc = rest cd_w_consts in + ty, pp, pp_doc, cd_w_consts + let declare { name; cname; doc; pp; compare; hash; hconsed; constants; } = - let cdata = declare { + let c = declare { data_compare = compare; data_pp = pp; data_hash = hash; data_name = cname; data_hconsed = hconsed; - } in - cdata, name, - List.fold_right (fun (n,v) -> - ED.Constants.Map.add (ED.Global_symbols.declare_global_symbol n) (n,v)) - constants ED.Constants.Map.empty, doc - - let build_conversion x = - let ty, pp, pp_doc = rest x in - { - Conversion.ty; - pp; - pp_doc; - embed = embed x; - readback = readback x; - } + } in + declare_cdata c name doc constants end @@ -618,53 +614,47 @@ end module BuiltInData = struct - let[@elpi.template] inline_data = fun name doc cdata constants constants_map -> - let { Util.CData.cin; isc; cout; name=c } = cdata in - let ty = Conversion.TyName name in - let embed ~depth:_ _ _ state x = - state, ED.Term.CData (cin x), [] in - let readback ~depth _ _ state t = - let module R = (val !r) in let open R in - match R.deref_head ~depth t with - | ED.Term.CData c when isc c -> state, cout c, [] - | ED.Term.Const i as t when i < 0 -> - begin try state, ED.Constants.Map.find i constants_map, [] - with Not_found -> raise (Conversion.TypeErr(ty,depth,t)) end - | t -> raise (Conversion.TypeErr(ty,depth,t)) in - let pp_doc fmt () = - let module R = (val !r) in let open R in - if doc <> "" then begin - ED.BuiltInPredicate.pp_comment fmt ("% " ^ doc); - Format.fprintf fmt "@\n"; - end; - Format.fprintf fmt "@[typeabbrev %s (ctype \"%s\").@]@\n@\n" name c; - List.iter (fun (c,_) -> - Format.fprintf fmt "@[type %s %s.@]@\n" c name) - constants in - { Conversion.embed; readback; ty; pp_doc; pp = (fun fmt x -> Util.CData.pp fmt (cin x)) } - - let int : 'h. (int, 'h) Conversion.t = [%elpi.template inline_data "int" "" ED.C.int [] ED.Constants.Map.empty] - let float : 'h. (float, 'h) Conversion.t = [%elpi.template inline_data "float" "" ED.C.float [] ED.Constants.Map.empty] - let string : 'h. (string, 'h) Conversion.t = [%elpi.template inline_data "string" "" ED.C.string [] ED.Constants.Map.empty] - let loc : 'h. (Util.Loc.t, 'h) Conversion.t = [%elpi.template inline_data "loc" "" ED.C.loc [] ED.Constants.Map.empty] - let char : 'h. (char, 'h) Conversion.t = [%elpi.template inline_data "char" "an octect" RawOpaqueData.char [] ED.Constants.Map.empty] - - let in_stream_constants = ["std_in",(stdin,"stdin")] - let in_stream_cmap = List.fold_left (fun m (c,v) -> - let c = ED.Global_symbols.declare_global_symbol c in - ED.Constants.Map.add c v m) - ED.Constants.Map.empty in_stream_constants - - let in_stream : 'h. (in_channel * string, 'h) Conversion.t = [%elpi.template inline_data "in_stream" "" RawOpaqueData.in_stream in_stream_constants in_stream_cmap] - - let out_stream_constants = ["std_out",(stdout,"stdout");"std_err",(stderr,"stderr")] - let out_stream_cmap = List.fold_left (fun m (c,v) -> - let c = ED.Global_symbols.declare_global_symbol c in - ED.Constants.Map.add c v m) - ED.Constants.Map.empty out_stream_constants - - let out_stream : 'h. (out_channel * string, 'h) Conversion.t = [%elpi.template inline_data "out_stream" "" RawOpaqueData.out_stream out_stream_constants out_stream_cmap] + let ty, pp, pp_doc, int = OpaqueData.declare_cdata RawOpaqueData.int "int" "" [] + let int : 'h. (int, 'h) Conversion.t = { Conversion.ty; pp; pp_doc; + embed = (fun ~depth -> OpaqueData.embed int ~depth); + readback = (fun ~depth -> OpaqueData.readback int ~depth); + } + let ty, pp, pp_doc, float = OpaqueData.declare_cdata RawOpaqueData.float "float" "" [] + let float : 'h. (float, 'h) Conversion.t = { Conversion.ty; pp; pp_doc; + embed = (fun ~depth -> OpaqueData.embed float ~depth); + readback = (fun ~depth -> OpaqueData.readback float ~depth); + } + + let ty, pp, pp_doc, string = OpaqueData.declare_cdata RawOpaqueData.string "string" "" [] + let string : 'h. (string, 'h) Conversion.t = { Conversion.ty; pp; pp_doc; + embed = (fun ~depth -> OpaqueData.embed string ~depth); + readback = (fun ~depth -> OpaqueData.readback string ~depth); + } + + let ty, pp, pp_doc, loc = OpaqueData.declare_cdata RawOpaqueData.loc "loc" "" [] + let loc : 'h. (Util.Loc.t, 'h) Conversion.t = { Conversion.ty; pp; pp_doc; + embed = (fun ~depth -> OpaqueData.embed loc ~depth); + readback = (fun ~depth -> OpaqueData.readback loc ~depth); + } + + let ty, pp, pp_doc, char = OpaqueData.declare_cdata RawOpaqueData.char "char" "an octect" [] + let char : 'h. (char, 'h) Conversion.t = { Conversion.ty; pp; pp_doc; + embed = (fun ~depth -> OpaqueData.embed char ~depth); + readback = (fun ~depth -> OpaqueData.readback char ~depth); + } + + let ty, pp, pp_doc, in_stream = OpaqueData.declare_cdata RawOpaqueData.in_stream "in_stream" "" ["std_in",(stdin,"stdin")] + let in_stream : 'h. (in_channel * string, 'h) Conversion.t = { Conversion.ty; pp; pp_doc; + embed = (fun ~depth -> OpaqueData.embed in_stream ~depth); + readback = (fun ~depth -> OpaqueData.readback in_stream ~depth); + } + + let ty, pp, pp_doc, out_stream = OpaqueData.declare_cdata RawOpaqueData.out_stream "out_stream" "" ["std_out",(stdout,"stdout");"std_err",(stderr,"stderr")] + let out_stream : 'h. (out_channel * string, 'h) Conversion.t = { Conversion.ty; pp; pp_doc; + embed = (fun ~depth -> OpaqueData.embed out_stream ~depth); + readback = (fun ~depth -> OpaqueData.readback out_stream ~depth); + } let poly ty = let embed ~depth:_ _ _ state x = state, x, [] in diff --git a/src/API.mli b/src/API.mli index 1a7b68bd9..95358de32 100644 --- a/src/API.mli +++ b/src/API.mli @@ -327,14 +327,26 @@ module OpaqueData : sig type 'a cdata_with_constants - val declare : 'a declaration -> 'a cdata_with_constants - val build_conversion : 'a cdata_with_constants -> ('a,'c) Conversion.t + val declare : 'a declaration -> + Conversion.ty_ast * (Format.formatter -> 'a -> unit) * (Format.formatter -> unit -> unit) * 'a cdata_with_constants - (* To circumvent value restriction you have assemble a Conversion.t by hand *) + (** To circumvent value restriction you have assemble a Conversion.t by + hand. Example (top level of a module): + + let ty, pp, pp_doc, name = declare { + name = "name"; + cname = "Names.Name.t"; + doc = "Name hints"; + pp = ... + } + let name : 'c. (Names.Name.t, #ctx as 'c) t= { ty; pp; pp_doc; + embed = (fun ~depth -> embed name ~depth); + readback = (fun ~depth -> readback name ~depth); + } + + *) val embed : 'a cdata_with_constants -> ('a,'c) Conversion.embedding val readback : 'a cdata_with_constants -> ('a,'c) Conversion.readback - val rest : 'a cdata_with_constants -> - Conversion.ty_ast * (Format.formatter -> 'a -> unit) * (Format.formatter -> unit -> unit) end @@ -403,7 +415,7 @@ module AlgebraicData : sig | S : ('bs,'b, 'ms, 'm, 'self, 'c) constructor_arguments -> ('self -> 'bs, 'self -> 'b, 'self -> 'ms, 'self -> 'm, 'self, 'c) constructor_arguments (* An argument of type `T 'self` for a constainer `T`, like a `list 'self`. `S args` above is a shortcut for `C(fun x -> x, args)` *) - | C : (('self,'c) Conversion.t -> ('a,'c) Conversion.t) * ('bs,'b,'ms,'m,'self, 'c) constructor_arguments -> ('a -> 'bs, 'a -> 'b, 'a -> 'ms,'a -> 'm, 'self, 'c) constructor_arguments + | C : (('self,Conversion.ctx) Conversion.t -> ('a,Conversion.ctx) Conversion.t) * ('bs,'b,'ms,'m,'self, 'c) constructor_arguments -> ('a -> 'bs, 'a -> 'b, 'a -> 'ms,'a -> 'm, 'self, 'c) constructor_arguments type ('t,'c) constructor = K : name * doc * @@ -420,7 +432,17 @@ module AlgebraicData : sig } constraint 'c = #Conversion.ctx - val declare : ('t,'c) declaration -> ('t,'c) Conversion.t + (** In order to obtain a quantification over the context one can do + as follows: + + let { ty; pp; pp_doc; embed; readback } = declare { ... } + let foo : 'c. (foo, #ctx as 'c) t = { ty; pp; pp_doc; + embed = (fun ~depth (c : #ctx) -> embed ~depth (c :> ctx)); + readback = (fun ~depth (c : #ctx) -> readback ~depth (c :> ctx)); + } + + *) + val declare : ('t,Conversion.ctx) declaration -> ('t,Conversion.ctx) Conversion.t end @@ -795,8 +817,8 @@ module BuiltInData : sig val string : (string, 'c) Conversion.t val list : ('a, 'c) Conversion.t -> ('a list, 'c) Conversion.t val loc : (Ast.Loc.t, 'c) Conversion.t - val bool : (bool, 'c) Conversion.t - val char : (char, 'c) Conversion.t + val bool : (bool, 'c) Conversion.t + val char : (char, 'c) Conversion.t (* The string is the "file name" *) val in_stream : (in_channel * string, 'c) Conversion.t val out_stream : (out_channel * string, 'c) Conversion.t diff --git a/src/builtin.ml b/src/builtin.ml index 3aa8c58d1..2a55ee152 100644 --- a/src/builtin.ml +++ b/src/builtin.ml @@ -919,7 +919,7 @@ let ctype = AlgebraicData.declare { ] } -let safe_wc = OpaqueData.declare { +let ty, pp, pp_doc, safe = OpaqueData.declare { OpaqueData.name = "safe"; cname = "safe"; pp = (fun fmt (id,l) -> @@ -931,12 +931,9 @@ let safe_wc = OpaqueData.declare { doc = "Holds data across bracktracking; can only contain closed terms"; constants = []; } -let ty, pp, pp_doc = OpaqueData.rest safe_wc -let safe : 'c. ('a, #Conversion.ctx as 'c) Conversion.t = -{ - Conversion.ty; pp; pp_doc; - embed = (fun ~depth -> OpaqueData.embed safe_wc ~depth); - readback = (fun ~depth -> OpaqueData.readback safe_wc ~depth); +let safe : 'c. ('a, #Conversion.ctx as 'c) Conversion.t = { Conversion.ty; pp; pp_doc; + embed = (fun ~depth -> OpaqueData.embed safe ~depth); + readback = (fun ~depth -> OpaqueData.readback safe ~depth); } let safeno = ref 0 @@ -1169,7 +1166,7 @@ let elpi_stdlib_src = let open BuiltIn in let open BuiltInData in [ let ocaml_set ~name (type a) (alpha : (a,Conversion.ctx) Conversion.t) (module Set : Util.Set.S with type elt = a) = -let set_wc = OpaqueData.declare { +let ty, pp, pp_doc, set = OpaqueData.declare { OpaqueData.name; cname = name; doc = ""; @@ -1179,11 +1176,9 @@ let set_wc = OpaqueData.declare { hconsed = false; constants = []; } in -let ty, pp, pp_doc = OpaqueData.rest set_wc in -let set : (Set.t, #Conversion.ctx as 'c) Conversion.t = { - Conversion.ty; pp; pp_doc; - embed = (fun ~depth -> OpaqueData.embed set_wc ~depth); - readback = (fun ~depth -> OpaqueData.readback set_wc ~depth); +let set : (Set.t, #Conversion.ctx as 'c) Conversion.t = { Conversion.ty; pp; pp_doc; + embed = (fun ~depth -> OpaqueData.embed set ~depth); + readback = (fun ~depth -> OpaqueData.readback set ~depth); } in let open BuiltIn in let open BuiltInData in let open Conversion in @@ -1280,7 +1275,7 @@ let ocaml_map ~name (type a) let closed_A = BuiltInData.closed "A" in -let map_wc = OpaqueData.declare { +let ty, pp, pp_doc, map = OpaqueData.declare { OpaqueData.name; cname = name; doc = ""; @@ -1290,12 +1285,11 @@ let map_wc = OpaqueData.declare { hconsed = false; constants = []; } in -let ty, pp, pp_doc = OpaqueData.rest map_wc in let map a = { Conversion.ty = Conversion.(TyApp(name,TyName a,[])); pp; pp_doc; - embed = (fun ~depth -> OpaqueData.embed map_wc ~depth); - readback = (fun ~depth -> OpaqueData.readback map_wc ~depth); + embed = (fun ~depth -> OpaqueData.embed map ~depth); + readback = (fun ~depth -> OpaqueData.readback map ~depth); } in let open BuiltIn in let open BuiltInData in let open Conversion in diff --git a/src/data.ml b/src/data.ml index 5b6062b7e..7a9e3b85a 100644 --- a/src/data.ml +++ b/src/data.ml @@ -719,7 +719,7 @@ type ('stateful_builder,'builder, 'stateful_matcher, 'matcher, 'self, 'ctx) con | S : ('bs,'b, 'ms, 'm, 'self, 'ctx) constructor_arguments -> ('self -> 'bs, 'self -> 'b, 'self -> 'ms, 'self -> 'm, 'self, 'ctx) constructor_arguments (* An argument of type `T 'self` for a constainer `T`, like a `list 'self`. `S args` above is a shortcut for `C(fun x -> x, args)` *) - | C : (('self,'ctx) Conversion.t -> ('a,'ctx) Conversion.t) * ('bs,'b,'ms,'m,'self, 'ctx) constructor_arguments -> ('a -> 'bs, 'a -> 'b, 'a -> 'ms,'a -> 'm, 'self, 'ctx) constructor_arguments + | C : (('self,Conversion.ctx) Conversion.t -> ('a,Conversion.ctx) Conversion.t) * ('bs,'b,'ms,'m,'self, 'ctx) constructor_arguments -> ('a -> 'bs, 'a -> 'b, 'a -> 'ms,'a -> 'm, 'self, 'ctx) constructor_arguments type ('t,'h) constructor = K : name * doc * @@ -759,10 +759,10 @@ let buildk ~mkConst kname = function | [] -> mkConst kname | x :: xs -> mkApp kname x xs -let rec readback_args : type a m t h. +let rec readback_args : type a m t. look:(depth:int -> term -> term) -> - Conversion.ty_ast -> depth:int -> h -> constraints -> State.t -> extra_goals list -> term -> - (a,m,t,h) compiled_constructor_arguments -> a -> term list -> + Conversion.ty_ast -> depth:int -> #Conversion.ctx -> constraints -> State.t -> extra_goals list -> term -> + (a,m,t,Conversion.ctx) compiled_constructor_arguments -> a -> term list -> State.t * t * extra_goals = fun ~look ty ~depth hyps constraints state extra origin args convert l -> match args, l with @@ -776,12 +776,12 @@ let rec readback_args : type a m t h. readback_args ~look ty ~depth hyps constraints state (gls :: extra) origin rest (convert x) xs -and readback : type t h. +and readback : type t. mkinterval:(int -> int -> int -> term list) -> look:(depth:int -> term -> term) -> alloc:(?name:string -> State.t -> State.t * 'uk) -> mkUnifVar:('uk -> args:term list -> State.t -> term) -> - Conversion.ty_ast -> (t,h) compiled_adt -> depth:int -> h -> constraints -> State.t -> term -> + Conversion.ty_ast -> (t,Conversion.ctx) compiled_adt -> depth:int -> #Conversion.ctx -> constraints -> State.t -> term -> State.t * t * extra_goals = fun ~mkinterval ~look ~alloc ~mkUnifVar ty adt ~depth hyps constraints state t -> try match look ~depth t with @@ -802,11 +802,11 @@ and readback : type t h. | _ -> raise (Conversion.TypeErr(ty,depth,t)) with Not_found -> raise (Conversion.TypeErr(ty,depth,t)) -and adt_embed_args : type m a t h. +and adt_embed_args : type m a t. mkConst:(int -> term) -> - Conversion.ty_ast -> (t,h) compiled_adt -> constant -> - depth:int -> h -> constraints -> - (a,m,t,h) compiled_constructor_arguments -> + Conversion.ty_ast -> (t,Conversion.ctx) compiled_adt -> constant -> + depth:int -> #Conversion.ctx -> constraints -> + (a,m,t,Conversion.ctx) compiled_constructor_arguments -> (State.t -> State.t * term * extra_goals) list -> m = fun ~mkConst ty adt kname ~depth hyps constraints args acc -> @@ -823,11 +823,11 @@ and adt_embed_args : type m a t h. adt_embed_args ~mkConst ty adt kname ~depth hyps constraints args ((fun state -> d.embed ~depth hyps constraints state x) :: acc) -and embed : type a h. +and embed : type a. mkConst:(int -> term) -> Conversion.ty_ast -> (Format.formatter -> a -> unit) -> - (a,h) compiled_adt -> - depth:int -> h -> constraints -> State.t -> + (a,Conversion.ctx) compiled_adt -> + depth:int -> #Conversion.ctx -> constraints -> State.t -> a -> State.t * term * extra_goals = fun ~mkConst ty pp adt -> let bindings = Constants.Map.bindings adt in @@ -842,7 +842,7 @@ and embed : type a h. aux bindings state let rec compile_arguments : type b bs m ms t. - (bs,b,ms,m,t,'h) constructor_arguments -> (t,#Conversion.ctx as 'h) Conversion.t -> (bs,ms,t,'h) compiled_constructor_arguments = + (bs,b,ms,m,t,Conversion.ctx) constructor_arguments -> (t,#Conversion.ctx) Conversion.t -> (bs,ms,t,Conversion.ctx) compiled_constructor_arguments = fun arg self -> match arg with | N -> XN diff --git a/src/dune b/src/dune index 20ef10cfe..336b1facf 100644 --- a/src/dune +++ b/src/dune @@ -20,11 +20,9 @@ ((action (run ppxfindcache_elpi_trace_deriving_std %{input-file} --ppx-opt --cookie --ppx-opt "elpi_trace=\"false\"" - --cache-file %{dep:.ppcache/API.ml} - --cache-file %{dep:.ppcache/API.mli} --cache-file %{dep:.ppcache/runtime_trace_off.ml} --cache-file %{dep:.ppcache/runtime_trace_off.mli})) - runtime_trace_off API) + runtime_trace_off) ((action (run camlp5o -I . -I +camlp5 pa_extend.cmo pa_lexer.cmo %{input-file})) parser) )) (libraries re.str camlp5.gramlib unix elpi.trace.runtime