11let elpi_stuff = ref []
22let pp_simple _ _ = ()
3- type simple = int [@@ deriving elpi { append = elpi_stuff }]
3+ type simple = int [@@ deriving elpi { declaration = elpi_stuff }]
44include
55 struct
66 [@@@ warning "-26-27-32-39-60" ]
77 let elpi_constant_type_simple = " simple"
88 let elpi_constant_type_simplec =
99 Elpi.API.RawData.Constants. declare_global_symbol
1010 elpi_constant_type_simple
11+ module Ctx_for_simple =
12+ struct class type t = object inherit Elpi.API.Conversion. ctx end end
1113 let rec elpi_embed_simple :
12- 'elpi__param__poly_hyps 'elpi__param__poly_csts .
13- (simple , 'elpi__param__poly_hyps , 'elpi__param__poly_csts )
14- Elpi.API.ContextualConversion. embedding
15- =
14+ 'c . (simple , #Ctx_for_simple. t as 'c ) Elpi.API.Conversion. embedding =
1615 fun ~depth ->
1716 fun h ->
1817 fun c -> fun s -> fun t -> Elpi.API.PPX. embed_int ~depth h c s t
1918 let rec elpi_readback_simple :
20- 'elpi__param__poly_hyps 'elpi__param__poly_csts .
21- (simple , 'elpi__param__poly_hyps , 'elpi__param__poly_csts )
22- Elpi.API.ContextualConversion. readback
23- =
19+ 'c . (simple , #Ctx_for_simple. t as 'c ) Elpi.API.Conversion. readback =
2420 fun ~depth ->
2521 fun h ->
2622 fun c -> fun s -> fun t -> Elpi.API.PPX. readback_int ~depth h c s t
27- let simple :
28- 'elpi__param__poly_hyps 'elpi__param__poly_csts .
29- (simple , 'elpi__param__poly_hyps , 'elpi__param__poly_csts )
30- Elpi.API.ContextualConversion. t
23+ let simple : 'c . (simple , #Ctx_for_simple. t as 'c ) Elpi.API.Conversion. t
3124 =
32- let kind = Elpi.API.ContextualConversion . TyName " simple" in
25+ let kind = Elpi.API.Conversion . TyName " simple" in
3326 {
34- Elpi.API.ContextualConversion . ty = kind;
27+ Elpi.API.Conversion . ty = kind;
3528 pp_doc =
3629 (fun fmt ->
3730 fun () -> Elpi.API.PPX.Doc. kind fmt kind ~doc: " simple" ; () );
@@ -45,18 +38,17 @@ include
4538 (" simple" ^
4639 (" " ^
4740 (((Elpi.API.PPX.Doc. show_ty_ast ~outer: false ) @@
48- (Elpi.API.ContextualConversion. (! > )
49- Elpi.API.BuiltInData. int ).Elpi.API.ContextualConversion. ty)
41+ Elpi.API.BuiltInData. int .Elpi.API.Conversion. ty)
5042 ^ (" . % " ^ " simple" )))))
51- let () =
52- elpi_stuff : =
53- (( ! elpi_stuff) @
54- ([elpi_simple] @
55- [ Elpi.API.BuiltIn. LPCode
56- ( String. concat " \n "
57- [ " pred map.simple i:simple, o:simple. " ;
58- Printf. sprintf " map.%s %sA B :- %s. " " simple " " "
59- ( " ( " ^ ( " (=) " ^ ( " " ^ ( " A " ^ ( " " ^ ( " B " ^ " ) " ))))))])]) )
43+ class ctx_for_simple ( h : Elpi.API.Data.hyps ) ( s : Elpi.API.Data.state )
44+ : Ctx_for_simple. t =
45+ object (_) inherit (( Elpi.API.Conversion. ctx) h) end
46+ let (in_ctx_for_simple :
47+ Ctx_for_simple. t Elpi.API.Conversion. ctx_readback) =
48+ fun ~ depth ->
49+ fun h ->
50+ fun c -> fun s -> (s, (( new ctx_for_simple) h s), ( List. concat [] ))
51+ let () = elpi_stuff := (( ! elpi_stuff) @ [elpi_simple] )
6052 end[@@ ocaml.doc " @inline" ][@@ merlin.hide ]
6153open Elpi.API
6254let builtin =
0 commit comments