instance attribute

Author: gares

lambdap.elpi

@@ -34,6 +34,12 @@ pred msolve o:list sealed-goal.
 % [lp.sig S T] Gives the type of a symbol
 external pred lp.sig i:symbol, o:term.
 
+% [lp.tc-instances L] Gives the list of type class instances
+external pred lp.tc-instances o:list symbol.
+
+% [lp.tc? S] Tells if S is a type class
+external pred lp.tc? i:symbol.
+
 % [lp.term->string T S] Pretty prints a term T to the string S
 external pred lp.term->string i:term, o:string.
 

src/core/sig_state.ml

@@ -46,13 +46,14 @@ let dummy : sig_state =
    [p], strategy [st], name [x], type [a], implicit arguments [impl] and
    optional definition [def]. This new symbol is returned too. *)
 let add_symbol : sig_state -> expo -> prop -> match_strat
-    -> bool -> strloc -> term -> bool list -> bool -> term option ->
+    -> bool -> strloc -> term -> bool list -> bool -> bool -> term option ->
       sig_state * sym =
-  fun ss expo prop mstrat opaq id typ impl tc def ->
+  fun ss expo prop mstrat opaq id typ impl tc tci def ->
   let sym =
     Sign.add_symbol ss.signature expo prop mstrat opaq id
       (cleanup typ) impl in
   if tc then Sign.add_tc ss.signature sym;
+  if tci then Sign.add_tc_inst ss.signature sym;
   begin
     match def with
     | Some t -> sym.sym_def := Some (cleanup t)

src/handle/command.ml

@@ -80,18 +80,19 @@ let handle_require_as : compiler -> sig_state -> p_path -> p_ident ->
 
 (** [handle_modifiers ms] verifies that the modifiers in [ms] are compatible.
     If so, they are returned as a tuple. Otherwise, it fails. *)
-let handle_modifiers : p_modifier list -> prop * expo * match_strat * bool =
+let handle_modifiers : p_modifier list -> prop * expo * match_strat * bool * bool =
   fun ms ->
-  let rec get_modifiers ((props, expos, strats,tc) as acc) = function
+  let rec get_modifiers ((props, expos, strats,tc,tci) as acc) = function
     | [] -> acc
-    | {elt=P_typeclass;_}::ms -> get_modifiers (props, expos, strats,true) ms
-    | {elt=P_prop _;_} as p::ms -> get_modifiers (p::props, expos, strats,tc) ms
-    | {elt=P_expo _;_} as e::ms -> get_modifiers (props, e::expos, strats,tc) ms
+    | {elt=P_typeclass;_}::ms -> get_modifiers (props, expos, strats,true, tci) ms
+    | {elt=P_typeclass_instance;_}::ms -> get_modifiers (props, expos, strats,tc, true) ms
+    | {elt=P_prop _;_} as p::ms -> get_modifiers (p::props, expos, strats,tc,tci) ms
+    | {elt=P_expo _;_} as e::ms -> get_modifiers (props, e::expos, strats,tc,tci) ms
     | {elt=P_mstrat _;_} as s::ms ->
-        get_modifiers (props, expos, s::strats,tc) ms
+        get_modifiers (props, expos, s::strats,tc,tci) ms
     | {elt=P_opaq;_}::ms -> get_modifiers acc ms
   in
-  let props, expos, strats, tc = get_modifiers ([],[],[],false) ms in
+  let props, expos, strats, tc, tci = get_modifiers ([],[],[],false,false) ms in
   let prop =
     match props with
     | [{elt=P_prop (Assoc b);_};{elt=P_prop Commu;_}]
@@ -120,7 +121,7 @@ let handle_modifiers : p_modifier list -> prop * expo * match_strat * bool =
     | [] -> Eager
     | _ -> assert false
   in
-  (prop, expo, strat, tc)
+  (prop, expo, strat, tc, tci)
 
 (** [check_rule ss syms r] checks rule [r] and returns the head symbol of the
    lhs and the rule itself. *)
@@ -164,7 +165,7 @@ let handle_inductive_symbol : sig_state -> expo -> prop -> match_strat
   end;
   (* Actually add the symbol to the signature and the state. *)
   Console.out 2 (Color.red "symbol %a : %a") uid name term typ;
-  let r = add_symbol ss expo prop mstrat false id typ impl false None in
+  let r = add_symbol ss expo prop mstrat false id typ impl false false None in
   sig_state := fst r; r
 
 (** Representation of a yet unchecked proof. The structure is initialized when
@@ -282,9 +283,11 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
 
   | P_inductive(ms, params, p_ind_list) ->
       (* Check modifiers. *)
-      let (prop, expo, mstrat,tc) = handle_modifiers ms in
+      let (prop, expo, mstrat,tc,tci) = handle_modifiers ms in
       if tc then
         fatal pos "Property typeclass cannot be used on inductive types.";
+      if tci then
+        fatal pos "Property instance cannot be used on inductive types.";
       if prop <> Defin then
         fatal pos "Property modifiers cannot be used on inductive types.";
       if mstrat <> Eager then
@@ -351,7 +354,8 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
           (* Recursors are declared after the types and constructors. *)
           let pos = after (end_pos pos) in
           let id = Pos.make pos rec_name in
-          let r = add_symbol ss expo Defin Eager false id rec_typ [] false None
+          let r =
+            add_symbol ss expo Defin Eager false id rec_typ [] false false None
           in sig_state := fst r; r
         in
         (ss, rec_sym::rec_sym_list)
@@ -389,7 +393,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
       | _ -> ()
     end;
     (* Verify modifiers. *)
-    let prop, expo, mstrat, tc = handle_modifiers p_sym_mod in
+    let prop, expo, mstrat, tc, tci = handle_modifiers p_sym_mod in
     let opaq = List.exists Syntax.is_opaq p_sym_mod in
     let pdata_prv = expo = Privat || (p_sym_def && opaq) in
     (match p_sym_def, opaq, prop, mstrat with
@@ -494,7 +498,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
             Console.out 2 (Color.red "symbol %a : %a") uid id term a;
             wrn pe.pos "Proof admitted.";
             let t = Option.map (fun t -> t.elt) t in
-            fst (add_symbol ss expo prop mstrat opaq p_sym_nam a impl tc t)
+            fst (add_symbol ss expo prop mstrat opaq p_sym_nam a impl tc tci t)
         | P_proof_end ->
             (* Check that the proof is indeed finished. *)
             if not (finished ps) then
@@ -504,7 +508,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
               Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term in
             (* Add the symbol in the signature. *)
             Console.out 2 (Color.red "symbol %a : %a") uid id term a;
-            fst (add_symbol ss expo prop mstrat opaq p_sym_nam a impl tc d)
+            fst (add_symbol ss expo prop mstrat opaq p_sym_nam a impl tc tci d)
       in
       (* Create the proof state. *)
       let pdata_state =

src/handle/elpi_handle.ml

@@ -2,6 +2,9 @@ open Elpi.API
 open Core
 open Elpi_lambdapi
 
+let ss : Sig_state.t State.component =
+  State.declare ~name:"elpi:ss"
+    ~pp:(fun _fmt _ -> ()) ~init:(fun () -> Sig_state.dummy) ~start:(fun x -> x)
 
 let goalc = RawData.Constants.declare_global_symbol "goal"
 let ofc = RawData.Constants.declare_global_symbol "of"
@@ -75,6 +78,23 @@ pred msolve o:list sealed-goal.
     (fun s _ ~depth:_ -> !: (Timed.(!) s.Term.sym_type))),
     DocAbove);
 
+  MLCode(Pred("lp.tc-instances",
+    Out(list sym,"L",
+    Read (ContextualConversion.unit_ctx, "Gives the list of type class instances")),
+    (fun _ ~depth:_ _ _ state ->
+      let s = (State.get ss state).Sig_state.signature in
+      !: ((Timed.(!) s.Sign.sign_tc_inst) |> Term.SymSet.elements))),
+    DocAbove);
+
+  MLCode(Pred("lp.tc?",
+    In(sym,"S",
+    Read (ContextualConversion.unit_ctx, "Tells if S is a type class")),
+    (fun sym ~depth:_ _ _ state ->
+      let s = (State.get ss state).Sig_state.signature in
+      if ((Timed.(!) s.Sign.sign_tc) |> Term.SymSet.mem sym) then ()
+      else raise No_clause)),
+    DocAbove);
+
   MLCode(Pred("lp.term->string",
     In(term,"T",
     Out(string,"S",
@@ -188,6 +208,13 @@ let tc_metas_of_term : Sig_state.t -> Term.ctxt -> Term.term -> Term.meta list =
 
 let scope_ref : (Parsing.Syntax.p_term -> Term.term * (int * string) list) ref = ref (fun _ -> assert false)
 
+(* we set the state, Elpi.API.Qery lacks this function *)
+let hack s c = { c with Conversion.embed =
+  fun ~depth state x ->
+    let state = State.set ss state s in
+    c.Conversion.embed ~depth state x
+}
+
 let solve_tc : ?scope:(Parsing.Syntax.p_term -> Term.term * (int * string) list) -> Sig_state.t -> Common.Pos.popt -> Term.problem -> Term.ctxt ->
   Term.term * Term.term -> Term.term * Term.term =
   fun ?scope ss pos _pb ctxt (t,ty) ->
@@ -213,7 +240,7 @@ let solve_tc : ?scope:(Parsing.Syntax.p_term -> Term.term * (int * string) list)
         let open Elpi.API.Query in
         let open Elpi.API.BuiltInData in
         compile prog pos
-          (Query { predicate; arguments = (D(list goal,tc,N)) }) in
+          (Query { predicate; arguments = (D(hack ss (list goal),tc,N)) }) in
 
       if not (Elpi.API.Compile.static_check
                 ~checker:(Elpi.Builtin.default_checker ()) query) then

src/handle/tactic.ml

@@ -38,7 +38,7 @@ let add_axiom : Sig_state.t -> popt -> meta -> Sig_state.t =
     in
     let id = Pos.make pos name in
     Sig_state.add_symbol
-      ss Public Defin Eager true id !(m.meta_type) [] false None
+      ss Public Defin Eager true id !(m.meta_type) [] false false None
   in
   (* Create the value which will be substituted for the metavariable. This
      value is [sym x0 ... xn] where [xi] are variables that will be

src/parsing/lpLexer.ml

@@ -56,6 +56,7 @@ type token =
   | INDUCTIVE
   | INFIX
   | INJECTIVE
+  | INSTANCE
   | LET
   | NOTATION
   | OPAQUE
@@ -221,6 +222,7 @@ let rec token lb =
   | "inductive" -> INDUCTIVE
   | "infix" -> INFIX
   | "injective" -> INJECTIVE
+  | "instance" -> INSTANCE
   | "left" -> SIDE(Pratter.Left)
   | "let" -> LET
   | "notation" -> NOTATION

src/parsing/lpParser.mly

@@ -49,6 +49,7 @@
 %token INDUCTIVE
 %token INFIX
 %token INJECTIVE
+%token INSTANCE
 %token LET
 %token NOTATION
 %token OPAQUE
@@ -207,6 +208,7 @@ modifier:
   | PROTECTED { make_pos $sloc (P_expo Term.Protec) }
   | SEQUENTIAL { make_pos $sloc (P_mstrat Term.Sequen) }
   | TYPECLASS { make_pos $sloc P_typeclass }
+  | INSTANCE { make_pos $sloc P_typeclass_instance }
 
 uid: s=UID { make_pos $sloc s}
 

src/parsing/syntax.ml

@@ -235,6 +235,7 @@ type p_modifier_aux =
   | P_prop of Term.prop (** symbol properties: constant, definable, ... *)
   | P_opaq (** opacity *)
   | P_typeclass
+  | P_typeclass_instance
 
 type p_modifier = p_modifier_aux loc
 

tcsolver.elpi

@@ -1,5 +1,5 @@
 msolve L :- 
-  compile_all [{{eqdec}}] Cl,
+  compile_all Cl,
   Cl => std.forall L (open tc).
 
 pred open i:(term -> term -> prop), i:sealed-goal.
@@ -12,15 +12,9 @@ open P (seal (goal Ctx Ty Wit)) :-
 :index(_ 4)
 pred tc o:term, o:term.
 
-pred is_typeclass o:term.
-is_typeclass {{eqdec}}.
-
-pred instances o:term o:list term.
-instances {{eqdec}} [{{bool_eqdec}}, {{nat_eqdec}}, {{pair_eqdec}}].
-
 pred compile i:term, i:list prop, i:term, o:prop.
 compile (prod (appl T U) F) TODO H (pi x\ C x) :-
-  is_typeclass T,
+  T = symb S, lp.tc? S,
   !,
   pi x\
     compile (F x) [tc (appl T U) x |TODO] (appl H x) (C x).
@@ -32,13 +26,9 @@ compile (prod _ F) TODO H (pi x\ C x) :-
 
 compile End TODO HD (tc End HD :- TODO).
 
-pred compile_all i:list term, o:list prop.
-compile_all Refs Props :-
-  std.map Refs instances LList,
-  std.flatten LList Candidates,
+pred compile_all o:list prop.
+compile_all Props :-
+  lp.tc-instances Candidates,
   std.map Candidates
-    (cand\claus\ sigma T\ sigma N\
-    cand = (symb N),
-    lp.sig N T,
-    compile T [] cand claus)
+    (N\claus\ sigma T\ lp.sig N T, compile T [] (symb N) claus)
     Props.

tests/OK/elpitest.lp

@@ -24,9 +24,9 @@ symbol mk_Pair [i] [j] : T i → T j → Pair i j;
 symbol pair : U → U → U;
 rule T (pair $i $j) ↪ Pair $i $j;
 
-/* instance */ symbol bool_eqdec : eqdec bool ≔ mk_eqdec eq_bool /* p */;
-/* instance */ symbol nat_eqdec  : eqdec nat ≔ mk_eqdec eq_nat /* p */;
-/* instance */ symbol pair_eqdec : Π i j, eqdec i → eqdec j → eqdec (pair i j);
+instance symbol bool_eqdec : eqdec bool ≔ mk_eqdec eq_bool /* p */;
+instance symbol nat_eqdec  : eqdec nat ≔ mk_eqdec eq_nat /* p */;
+instance symbol pair_eqdec : Π i j, eqdec i → eqdec j → eqdec (pair i j);
   /* ≔ mk_eqdec eq_nat ; */
 
 type λ b , true == b;