move metadata to signature

gares · gares · commit f4b1f1e7f3f3 · 2023-01-26T15:33:17.000+01:00
diff --git a/lambdap.elpi b/lambdap.elpi
diff --git a/src/core/coercion.ml b/src/core/coercion.ml
@@ -3,7 +3,7 @@ open Term
 
 let coerce : sym =
   let id = Pos.none "coerce" in
-  Sign.add_symbol Ghost.sign Public Defin Eager false id mk_Kind [] false
+  Sign.add_symbol Ghost.sign Public Defin Eager false id mk_Kind []
 
 let apply a b t : term = add_args (mk_Symb coerce) [a; b; t]
 
diff --git a/src/core/sig_state.ml b/src/core/sig_state.ml
@@ -51,7 +51,8 @@ let add_symbol : sig_state -> expo -> prop -> match_strat
   fun ss expo prop mstrat opaq id typ impl tc def ->
   let sym =
     Sign.add_symbol ss.signature expo prop mstrat opaq id
-      (cleanup typ) impl tc in
+      (cleanup typ) impl in
+  if tc then Sign.add_tc ss.signature sym;
   begin
     match def with
     | Some t -> sym.sym_def := Some (cleanup t)
diff --git a/src/core/sign.ml b/src/core/sign.ml
@@ -36,6 +36,8 @@ type t =
   ; sign_notations: float notation SymMap.t ref
   (** Maps symbols to their notation if they have some. *)
   ; sign_ind      : ind_data SymMap.t ref
+  ; sign_tc       : SymSet.t ref
+  ; sign_tc_inst  : SymSet.t ref
   ; sign_cp_pos   : cp_pos list SymMap.t ref
   (** Maps a symbol to the critical pair positions it is heading in the
      rules. *) }
@@ -51,6 +53,7 @@ let dummy : unit -> t = fun () ->
   { sign_symbols = ref StrMap.empty; sign_path = []
   ; sign_deps = ref Path.Map.empty; sign_builtins = ref StrMap.empty
   ; sign_notations = ref SymMap.empty; sign_ind = ref SymMap.empty
+  ; sign_tc = ref SymSet.empty; sign_tc_inst = ref SymSet.empty
   ; sign_cp_pos = ref SymMap.empty }
 
 (** [find sign name] finds the symbol named [name] in [sign] if it exists, and
@@ -212,11 +215,11 @@ let unlink : t -> unit = fun sign ->
    arguments [impl], no definition and no rules. [name] should not already be
    used in [sign]. The created symbol is returned. *)
 let add_symbol : t -> expo -> prop -> match_strat -> bool -> strloc -> term ->
-      bool list -> bool -> sym =
-  fun sign sym_expo sym_prop sym_mstrat sym_opaq name typ impl sym_tc ->
+      bool list -> sym =
+  fun sign sym_expo sym_prop sym_mstrat sym_opaq name typ impl ->
   let sym =
     create_sym sign.sign_path sym_expo sym_prop sym_mstrat sym_opaq name
-      (cleanup typ) (minimize_impl impl) sym_tc
+      (cleanup typ) (minimize_impl impl)
   in
   sign.sign_symbols := StrMap.add name.elt sym !(sign.sign_symbols);
   sym
@@ -265,6 +268,8 @@ let read : string -> t = fun fname ->
   unsafe_reset sign.sign_notations;
   unsafe_reset sign.sign_ind;
   unsafe_reset sign.sign_cp_pos;
+  unsafe_reset sign.sign_tc;
+  unsafe_reset sign.sign_tc_inst;
   let shallow_reset_sym s =
     unsafe_reset s.sym_type;
     unsafe_reset s.sym_def;
@@ -301,6 +306,8 @@ let read : string -> t = fun fname ->
   StrMap.iter (fun _ s -> reset_sym s) !(sign.sign_symbols);
   StrMap.iter (fun _ s -> shallow_reset_sym s) !(sign.sign_builtins);
   SymMap.iter (fun s _ -> shallow_reset_sym s) !(sign.sign_notations);
+  SymSet.iter (fun s -> reset_sym s) !(sign.sign_tc);
+  SymSet.iter (fun s -> reset_sym s) !(sign.sign_tc_inst);
   let f _ sm = StrMap.iter (fun _ rs -> List.iter reset_rule rs) sm in
   Path.Map.iter f !(sign.sign_deps);
   let reset_ind i =
@@ -382,3 +389,12 @@ let rec dependencies : t -> (Path.t * t) list = fun sign ->
     | d::deps -> minimize ((List.filter not_here d) :: acc) deps
   in
   List.concat (minimize [] deps)
+
+let add_tc : t -> sym -> unit =
+  fun sign sym ->
+    sign.sign_tc := SymSet.add sym !(sign.sign_tc)
+
+let add_tc_inst : t -> sym -> unit =
+  fun sign sym ->    
+    sign.sign_tc_inst := SymSet.add sym !(sign.sign_tc_inst);
+  
diff --git a/src/core/term.ml b/src/core/term.ml
@@ -97,7 +97,6 @@ and sym =
   ; sym_rules : rule list ref (** Rewriting rules. *)
   ; sym_mstrat: match_strat (** Matching strategy. *)
   ; sym_dtree : dtree ref (** Decision tree used for matching. *)
-  ; sym_tc    : bool (** Type class *)
   ; sym_pos   : Pos.popt (** Position in source file. *) }
 
 (** {b NOTE} {!field:sym_type} holds a (timed) reference for a  technical
@@ -356,12 +355,12 @@ let new_problem : unit -> problem = fun () ->
    strategy [mstrat], name [name.elt], type [typ], implicit arguments [impl],
    position [name.pos], no definition and no rules. *)
 let create_sym : Path.t -> expo -> prop -> match_strat -> bool ->
-  Pos.strloc -> term -> bool list -> bool -> sym =
+  Pos.strloc -> term -> bool list -> sym =
   fun sym_path sym_expo sym_prop sym_mstrat sym_opaq
-    { elt = sym_name; pos = sym_pos } typ sym_impl sym_tc ->
+    { elt = sym_name; pos = sym_pos } typ sym_impl ->
   {sym_path; sym_name; sym_type = ref typ; sym_impl; sym_def = ref None;
    sym_opaq; sym_rules = ref []; sym_dtree = ref Tree_type.empty_dtree;
-   sym_mstrat; sym_prop; sym_expo; sym_pos; sym_tc }
+   sym_mstrat; sym_prop; sym_expo; sym_pos }
 
 (** [is_constant s] tells whether [s] is a constant. *)
 let is_constant : sym -> bool = fun s -> s.sym_prop = Const
@@ -378,9 +377,6 @@ let is_private : sym -> bool = fun s -> s.sym_expo = Privat
 let is_modulo : sym -> bool = fun s ->
   match s.sym_prop with Assoc _ | Commu | AC _ -> true | _ -> false
 
-(* [is_tc s] tells whether the symbol [s] is a type class *)
-let is_tc : sym -> bool = fun s -> s.sym_tc
-
 (** [unfold t] repeatedly unfolds the definition of the surface constructor of
     [t], until a significant {!type:term} constructor is found.  The term that
     is returned cannot be an instantiated metavariable or term environment nor
@@ -562,8 +558,7 @@ let right_aliens : sym -> term -> term list = fun s ->
 
 (* unit test *)
 let _ =
-  let s =
-    create_sym [] Privat (AC true) Eager false (Pos.none "+") Kind [] false in
+  let s = create_sym [] Privat (AC true) Eager false (Pos.none "+") Kind [] in
   let t1 = Vari (new_tvar "x1") in
   let t2 = Vari (new_tvar "x2") in
   let t3 = Vari (new_tvar "x3") in
diff --git a/src/core/term.mli b/src/core/term.mli
@@ -96,7 +96,6 @@ and sym =
   ; sym_rules : rule list ref (** Rewriting rules. *)
   ; sym_mstrat: match_strat (** Matching strategy. *)
   ; sym_dtree : dtree ref (** Decision tree used for matching. *)
-  ; sym_tc    : bool (** Type class *)
   ; sym_pos   : Pos.popt (** Position in source file. *) }
 
 (** {b NOTE} that {!field:sym_type} holds a (timed) reference for a  technical
@@ -301,7 +300,7 @@ module SymMap : Map.S with type key = sym
    arguments [impl], position [name.pos], typeclass [tc] no definition and no
    rules. *)
 val create_sym : Path.t -> expo -> prop -> match_strat -> bool ->
-  Pos.strloc -> term -> bool list -> bool -> sym
+  Pos.strloc -> term -> bool list -> sym
 
 (** [is_constant s] tells whether the symbol is a constant. *)
 val is_constant : sym -> bool
@@ -316,9 +315,6 @@ val is_private : sym -> bool
 (** [is_modulo s] tells whether the symbol [s] is modulo some equations. *)
 val is_modulo : sym -> bool
 
-(* [is_tc s] tells whether the symbol [s] is a type class *)
-val is_tc : sym -> bool
-
 (** Sets and maps of metavariables. *)
 module Meta : Map.OrderedType with type t = meta
 module MetaSet : Set.S with type elt = Meta.t
diff --git a/src/core/unif_rule.ml b/src/core/unif_rule.ml
@@ -11,14 +11,14 @@ open Term
 let equiv : sym =
   let id = Pos.none "≡" in
   let s =
-    Sign.add_symbol Ghost.sign Public Defin Eager false id mk_Kind [] false in
+    Sign.add_symbol Ghost.sign Public Defin Eager false id mk_Kind [] in
   Sign.add_notation Ghost.sign s (Infix(Pratter.Neither, 2.0)); s
 
 (** Symbol ";". *)
 let cons : sym =
   let id = Pos.none ";" in
   let s =
-    Sign.add_symbol Ghost.sign Public Const Eager true id mk_Kind [] false in
+    Sign.add_symbol Ghost.sign Public Const Eager true id mk_Kind [] in
   Sign.add_notation Ghost.sign s (Infix(Pratter.Right, 1.0)); s
 
 (** [unpack eqs] transforms a term of the form
diff --git a/src/handle/elpi_handle.ml b/src/handle/elpi_handle.ml
@@ -142,9 +142,12 @@ fun ss file predicate arg ->
 
 let extend (cctx) v ?def ty = (v, ty, def) :: cctx
 
-let is_tc_instance : Term.ctxt -> Term.meta -> bool = fun c m ->
+let is_tc_instance : Sig_state.t -> Term.ctxt -> Term.meta -> bool =
+  fun ss c m ->
   let open Timed in
   let open Term in
+  let is_tc symb  =
+    SymSet.mem symb !(ss.Sig_state.signature.Sign.sign_tc) in
   let rec aux c t =
     match get_args (unfold t) with
     | Symb s, _ -> is_tc s
@@ -156,12 +159,13 @@ let is_tc_instance : Term.ctxt -> Term.meta -> bool = fun c m ->
   in
     aux c !(m.meta_type)
 
-let tc_metas_of_term : Term.ctxt -> Term.term -> Term.meta list = fun c t ->
+let tc_metas_of_term : Sig_state.t -> Term.ctxt -> Term.term -> Term.meta list =
+  fun ss c t ->
   let open Term in
   let acc = ref [] in
   let rec aux c t =
     match unfold t with
-    | Meta(m,_) when is_tc_instance c m && not (List.memq m !acc) ->
+    | Meta(m,_) when is_tc_instance ss c m && not (List.memq m !acc) ->
        acc := m :: !acc
     | Abst (dom, b) | Prod(dom, b) ->
        aux c dom;
@@ -184,10 +188,10 @@ let tc_metas_of_term : Term.ctxt -> Term.term -> Term.meta list = fun c t ->
 
 let scope_ref : (Parsing.Syntax.p_term -> Term.term * (int * string) list) ref = ref (fun _ -> assert false)
 
-let solve_tc : ?scope:(Parsing.Syntax.p_term -> Term.term * (int * string) list) -> Common.Pos.popt -> Term.problem -> Term.ctxt ->
+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 pos _pb ctxt (t,ty) ->
-    let tc = tc_metas_of_term ctxt t in
+  fun ?scope ss pos _pb ctxt (t,ty) ->
+    let tc = tc_metas_of_term ss ctxt t in
     if tc <> [] then begin
       let elpi = match !elpi with None -> assert false | Some x -> x in
       Option.iter (fun f -> scope_ref := f) scope;
diff --git a/src/handle/query.ml b/src/handle/query.ml
@@ -7,15 +7,15 @@ open Proof
 open Lplib open Base
 open Timed
 
-let infer : ?scope:(Parsing.Syntax.p_term -> Term.term * (int * string) list) -> Pos.popt -> problem -> ctxt -> term -> term * term =
-  fun ?scope pos p ctx t ->
+let infer : ?scope:(Parsing.Syntax.p_term -> Term.term * (int * string) list) -> Sig_state.t -> Pos.popt -> problem -> ctxt -> term -> term * term =
+  fun ?scope ss pos p ctx t ->
   match Infer.infer_noexn p ctx t with
   | None -> fatal pos "%a is not typable." term t
   | Some (t, a) ->
       if Unif.solve_noexn p then
         begin
           if !p.unsolved = [] then begin
-            let t, a = Elpi_handle.solve_tc ?scope pos p ctx (t, a) in
+            let t, a = Elpi_handle.solve_tc ?scope ss pos p ctx (t, a) in
             match Infer.infer_noexn p ctx t with
             | None -> fatal pos "%a is not typable AFTER TC RESOLUTION!!!!" term t
             | _ -> Common.Console.out 1 "TC RESOLUTION OK!@ ";
@@ -184,9 +184,9 @@ let handle : Sig_state.t -> proof_state option -> p_query -> result =
       Console.out 2 "assertion: it is %b that %a" (not must_fail)
         constr (ctxt, t, u);
       (* Check that [t] is typable. *)
-      let (t, a) = infer pt.pos p ctxt t in
+      let (t, a) = infer ss pt.pos p ctxt t in
       (* Check that [u] is typable. *)
-      let (u, b) = infer pu.pos p ctxt u in
+      let (u, b) = infer ss pu.pos p ctxt u in
       (* Check that [t] and [u] have the same type. *)
       p := {!p with to_solve = (ctxt,a,b)::!p.to_solve};
       if Unif.solve_noexn p then
@@ -206,11 +206,11 @@ let handle : Sig_state.t -> proof_state option -> p_query -> result =
   | P_query_infer(pt, cfg) ->
       let t = scope pt in
       let scope = Scope.scope_term_w_pats ~typ:false ~mok true ss env in
-      let t, ty = infer ~scope pt.pos p ctxt t in
+      let t, ty = infer ss ~scope pt.pos p ctxt t in
       let t = Eval.eval cfg ctxt t in
       let ty = Eval.eval cfg ctxt ty in
       return typing (ctxt,t,ty)
   | P_query_normalize(pt, cfg) ->
       let t = scope pt in
-      let t, _ = infer pt.pos p ctxt t in
+      let t, _ = infer ss pt.pos p ctxt t in
       return term (Eval.eval cfg ctxt t)
diff --git a/src/handle/query.mli b/src/handle/query.mli
@@ -10,7 +10,7 @@ open Proof
     refinement of [t]. Note that [p] gets modified. Context [c] must well
     sorted.
     @raise Fatal if [t] cannot be typed. *)
-val infer : ?scope:(Parsing.Syntax.p_term -> Core.Term.term * (int * string) list) -> popt -> problem -> ctxt -> term -> term * term
+val infer : ?scope:(Parsing.Syntax.p_term -> Core.Term.term * (int * string) list) -> Sig_state.t -> popt -> problem -> ctxt -> term -> term * term
 
 (** [check pos p c t a] checks that the term [t] has type [a] in context [c]
     and under the constraints of [p], and returns [t] refined. Context [c]
diff --git a/src/handle/rewrite.ml b/src/handle/rewrite.ml
@@ -321,7 +321,7 @@ let rewrite : Sig_state.t -> problem -> popt -> goal_typ -> bool ->
 
   (* Infer the type of [t] (the argument given to the tactic). *)
   let g_ctxt = Env.to_ctxt g_env in
-  let (t, t_type) = Query.infer pos p g_ctxt t in
+  let (t, t_type) = Query.infer ss pos p g_ctxt t in
 
   (* Check that [t_type ≡ Π x1:a1, ..., Π xn:an, P (eq a l r)]. *)
   let (a, l, r), vars  = get_eq_data cfg pos t_type in
diff --git a/src/handle/why3_tactic.ml b/src/handle/why3_tactic.ml
@@ -288,7 +288,7 @@ let handle :
   (* Add the axiom to the current signature. *)
   let a =
     Sign.add_symbol ss.signature Public Defin Eager true
-      (Pos.make pos axiom_name) !(m.meta_type) [] false
+      (Pos.make pos axiom_name) !(m.meta_type) []
   in
   if Logger.log_enabled () then
     log_why3 "axiom %a created" uid axiom_name;
diff --git a/src/tool/lcr.ml b/src/tool/lcr.ml
@@ -277,7 +277,7 @@ let _ =
   let v0 = var 0
   and v1 = var 1 in
   let sym name =
-    create_sym [] Public Defin Eager false (Pos.none name) mk_Type [] false in
+    create_sym [] Public Defin Eager false (Pos.none name) mk_Type [] in
   let a_ = sym "a"
   and b_ = sym "b"
   and s_ = sym "s"
@@ -428,7 +428,7 @@ let typability_constraints : Pos.popt -> term -> subs option = fun pos t ->
     try
       let i,n = MetaMap.find m !m2p in
       let s = create_sym (Sign.current_path())
-          Public Defin Eager false (Pos.none n) mk_Kind [] false in
+          Public Defin Eager false (Pos.none n) mk_Kind [] in
       let t = Bindlib.unbox (Bindlib.bind_mvar [||] (_Symb s)) in
       Timed.(m.meta_value := Some t);
       s2p := SymMap.add s i !s2p
diff --git a/src/tool/sr.ml b/src/tool/sr.ml
@@ -204,7 +204,7 @@ let check_rule : Scope.pre_rule Pos.loc -> rule = fun ({pos; elt} as pr) ->
         let s =
           let name = Pos.none @@ Printf.sprintf "$%d" m.meta_key in
           Term.create_sym (Sign.current_path()) Privat Defin Eager
-            false name !(m.meta_type) [] false in
+            false name !(m.meta_type) [] in
         Stdlib.(symbols := s :: !symbols);
         (* Build a definition for [m]. *)
         let xs = Array.init m.meta_arity (new_tvar_ind "x") in
diff --git a/tests/rewriting.ml b/tests/rewriting.ml
@@ -15,7 +15,7 @@ let scope_term ss = Scope.scope_term true ss []
 
 let add_sym ss id =
   Sig_state.add_symbol ss Public Defin Eager true (Pos.none id) Term.mk_Kind []
-    None
+    false None
 
 (* Define a signature state and some symbols. *)
 
