Remove prototype type-classes implementation.

Co-authored-by: Gustavo Delerue <gxdelerue@proton.me>
Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu>

Author: Gustavo2622

src/ecCallbyValue.ml

@@ -300,7 +300,7 @@ and try_reduce_fixdef
 
     let body = EcFol.form_of_expr body in
     let body =
-      Tvar.f_subst ~freshen:true (List.map fst op.EcDecl.op_tparams) tys body in
+      Tvar.f_subst ~freshen:true op.EcDecl.op_tparams tys body in
 
     Some (cbv st subst body (Args.create ty eargs))
 

src/ecCommands.ml

@@ -418,13 +418,6 @@ and process_subtype (scope : EcScope.scope) (subtype : psubtype located) =
   EcScope.notify scope `Info "added subtype: `%s'" (unloc subtype.pl_desc.pst_name);
   scope
 
-(* -------------------------------------------------------------------- *)
-and process_typeclass (scope : EcScope.scope) (tcd : ptypeclass located) =
-  EcScope.check_state `InTop "type class" scope;
-  let scope = EcScope.Ty.add_class scope tcd in
-    EcScope.notify scope `Info "added type class: `%s'" (unloc tcd.pl_desc.ptc_name);
-    scope
-
 (* -------------------------------------------------------------------- *)
 and process_tycinst (scope : EcScope.scope) (tci : ptycinstance located) =
   EcScope.check_state `InTop "type class instance" scope;
@@ -758,7 +751,6 @@ and process ?(src : string option) (ld : Loader.loader) (scope : EcScope.scope)
       match g.pl_desc with
       | Gtype        t    -> `Fct   (fun scope -> process_types      ?src scope  (List.map (mk_loc loc) t))
       | Gsubtype     t    -> `Fct   (fun scope -> process_subtype    scope  (mk_loc loc t))
-      | Gtypeclass   t    -> `Fct   (fun scope -> process_typeclass  scope  (mk_loc loc t))
       | Gtycinstance t    -> `Fct   (fun scope -> process_tycinst    scope  (mk_loc loc t))
       | Gmodule      m    -> `Fct   (fun scope -> process_module     ?src scope m)
       | Ginterface   i    -> `Fct   (fun scope -> process_interface  ?src scope i)

src/ecDecl.ml

@@ -11,7 +11,7 @@ module Ssym = EcSymbols.Ssym
 module CS   = EcCoreSubst
 
 (* -------------------------------------------------------------------- *)
-type ty_param  = EcIdent.t * EcPath.Sp.t
+type ty_param  = EcIdent.t
 type ty_params = ty_param list
 type ty_pctor  = [ `Int of int | `Named of ty_params ]
 
@@ -29,7 +29,7 @@ type ty_dtype = {
 
 type ty_body = 
   | Concrete of EcTypes.ty
-  | Abstract of Sp.t
+  | Abstract
   | Datatype of ty_dtype
   | Record   of ty_record
 
@@ -44,7 +44,7 @@ let tydecl_as_concrete (td : tydecl) =
   match td.tyd_type with Concrete x -> Some x | _ -> None
 
 let tydecl_as_abstract (td : tydecl) =
-  match td.tyd_type with Abstract x -> Some x | _ -> None
+  match td.tyd_type with Abstract -> Some () | _ -> None
 
 let tydecl_as_datatype (td : tydecl) =
   match td.tyd_type with Datatype x -> Some x | _ -> None
@@ -53,23 +53,23 @@ let tydecl_as_record (td : tydecl) =
   match td.tyd_type with Record (x, y) -> Some (x, y) | _ -> None
 
 (* -------------------------------------------------------------------- *)
-let abs_tydecl ?(tc = Sp.empty) ?(params = `Int 0) lc =
+let abs_tydecl ?(params = `Int 0) lc =
   let params =
     match params with
     | `Named params ->
         params
     | `Int n ->
         let fmt = fun x -> Printf.sprintf "'%s" x in
         List.map
-          (fun x -> (EcIdent.create x, Sp.empty))
+          (fun x -> (EcIdent.create x))
           (EcUid.NameGen.bulk ~fmt n)
   in
 
-  { tyd_params = params; tyd_type = Abstract tc; tyd_loca = lc; }
+  { tyd_params = params; tyd_type = Abstract; tyd_loca = lc; }
 
 (* -------------------------------------------------------------------- *)
 let ty_instantiate (params : ty_params) (args : ty list) (ty : ty) =
-  let subst = CS.Tvar.init (List.map fst params) args in
+  let subst = CS.Tvar.init params args in
   CS.Tvar.subst subst ty
 
 (* -------------------------------------------------------------------- *)
@@ -254,12 +254,19 @@ let operator_as_prind (op : operator) =
   | _ -> assert false
 
 (* -------------------------------------------------------------------- *)
-let axiomatized_op ?(nargs = 0) ?(nosmt = false) path (tparams, axbd) lc =
+let axiomatized_op 
+  ?(nargs = 0) 
+  ?(nosmt = false) 
+  (path : EcPath.path)
+  ((tparams, axbd) : ty_params * form)
+  (lc : locality)
+  : axiom
+=
   let axbd, axpm =
-    let bdpm = List.map fst tparams in
+    let bdpm = tparams in
     let axpm = List.map EcIdent.fresh bdpm in
       (CS.Tvar.f_subst ~freshen:true bdpm (List.map EcTypes.tvar axpm) axbd,
-       List.combine axpm (List.map snd tparams))
+       axpm)
   in
 
   let args, axbd =
@@ -271,7 +278,7 @@ let axiomatized_op ?(nargs = 0) ?(nosmt = false) path (tparams, axbd) lc =
   in
 
   let opargs = List.map (fun (x, ty) -> f_local x (gty_as_ty ty)) args in
-  let tyargs = List.map (EcTypes.tvar |- fst) axpm in
+  let tyargs = List.map EcTypes.tvar axpm in
   let op     = f_op path tyargs (toarrow (List.map f_ty opargs) axbd.EcAst.f_ty) in
   let op     = f_app op opargs axbd.f_ty in
   let axspec = f_forall args (f_eq op axbd) in

src/ecDecl.mli

@@ -2,12 +2,11 @@
 open EcUtils
 open EcSymbols
 open EcBigInt
-open EcPath
 open EcTypes
 open EcCoreFol
 
 (* -------------------------------------------------------------------- *)
-type ty_param  = EcIdent.t * EcPath.Sp.t
+type ty_param  = EcIdent.t
 type ty_params = ty_param list
 type ty_pctor  = [ `Int of int | `Named of ty_params ]
 
@@ -25,7 +24,7 @@ type ty_dtype = {
 
 type ty_body = 
   | Concrete of EcTypes.ty
-  | Abstract of Sp.t
+  | Abstract
   | Datatype of ty_dtype
   | Record   of ty_record
 
@@ -37,11 +36,11 @@ type tydecl = {
 }
 
 val tydecl_as_concrete : tydecl -> EcTypes.ty option
-val tydecl_as_abstract : tydecl -> Sp.t option
+val tydecl_as_abstract : tydecl -> unit option
 val tydecl_as_datatype : tydecl -> ty_dtype option
 val tydecl_as_record   : tydecl -> (form * (EcSymbols.symbol * EcTypes.ty) list) option
 
-val abs_tydecl : ?tc:Sp.t -> ?params:ty_pctor -> locality -> tydecl
+val abs_tydecl : ?params:ty_pctor -> locality -> tydecl
 
 val ty_instantiate : ty_params -> ty list -> ty -> ty
 

src/ecEnv.ml

@@ -782,13 +782,13 @@ module MC = struct
 
       match tyd.tyd_type with
       | Concrete _  -> mc
-      | Abstract _ -> mc
+      | Abstract    -> mc
 
       | Datatype dtype ->
           let cs      = dtype.tydt_ctors   in
           let schelim = dtype.tydt_schelim in
           let schcase = dtype.tydt_schcase in
-          let params  = List.map (fun (x, _) -> tvar x) tyd.tyd_params in
+          let params  = List.map tvar tyd.tyd_params in
           let for1 i (c, aty) =
             let aty = EcTypes.toarrow aty (tconstr mypath params) in
             let aty = EcSubst.freshen_type (tyd.tyd_params, aty) in
@@ -829,7 +829,7 @@ module MC = struct
             ) mc projs
 
       | Record (scheme, fields) ->
-          let params  = List.map (fun (x, _) -> tvar x) tyd.tyd_params in
+          let params  = List.map tvar tyd.tyd_params in
           let nfields = List.length fields in
           let cfields =
             let for1 i (f, aty) =
@@ -911,7 +911,7 @@ module MC = struct
           let opname = EcIdent.name opid in
           let optype = EcSubst.subst_ty tsubst optype in
           let opdecl =
-            mk_op ~opaque:optransparent [(self, Sp.singleton mypath)]
+            mk_op ~opaque:optransparent [(self)]
               optype (Some OP_TC) loca
           in (opid, xpath opname, optype, opdecl)
         in
@@ -931,7 +931,7 @@ module MC = struct
         List.map
           (fun (x, ax) ->
             let ax = EcSubst.subst_form fsubst ax in
-              (x, { ax_tparams = [(self, Sp.singleton mypath)];
+              (x, { ax_tparams = [(self)];
                     ax_spec    = ax;
                     ax_kind    = `Lemma;
                     ax_loca    = loca;
@@ -1107,9 +1107,6 @@ module MC = struct
         else
           (add2mc _up_theory xsubth cth mc, None)
 
-      | Th_typeclass (x, tc) ->
-          (add2mc _up_typeclass x tc mc, None)
-
       | Th_baserw (x, _) ->
           (add2mc _up_rwbase x (expath x) mc, None)
 
@@ -1406,11 +1403,6 @@ module TypeClass = struct
           let myself = EcPath.pqname (root env) name in
             { env with env_tc = TC.Graph.add ~src:myself ~dst:prt env.env_tc }
 
-  let bind ?(import = true) name tc env =
-    let env = rebind name tc env in
-    let item = Th_typeclass (name, tc) in
-    { env with env_item = mkitem ~import item :: env.env_item }
-
   let lookup qname (env : env) =
     MC.lookup_typeclass qname env
 
@@ -2548,7 +2540,7 @@ module Ty = struct
     match by_path_opt name env with
     | Some ({ tyd_type = Concrete body } as tyd) ->
         Tvar.subst
-          (Tvar.init (List.map fst tyd.tyd_params) args)
+          (Tvar.init tyd.tyd_params args)
           body
     | _ -> raise (LookupFailure (`Path name))
 
@@ -2603,22 +2595,7 @@ module Ty = struct
     | _ -> None
 
   let rebind name ty env =
-    let env = MC.bind_tydecl name ty env in
-
-    match ty.tyd_type with
-    | Abstract tc ->
-        let myty =
-          let myp = EcPath.pqname (root env) name in
-          let typ = List.map (fst_map EcIdent.fresh) ty.tyd_params in
-            (typ, EcTypes.tconstr myp (List.map (tvar |- fst) typ)) in
-        let instr =
-          Sp.fold
-            (fun p inst -> TypeClass.bind_instance myty (`General p) inst)
-            tc env.env_tci
-        in
-          { env with env_tci = instr }
-
-    | _ -> env
+    MC.bind_tydecl name ty env
 
   let bind ?(import = true) name ty env =
     let env = rebind name ty env in
@@ -2722,7 +2699,7 @@ module Op = struct
 
   let reduce ?mode ?nargs env p tys =
     let op, f = core_reduce ?mode ?nargs env p in
-    Tvar.f_subst ~freshen:true (List.map fst op.op_tparams) tys f
+    Tvar.f_subst ~freshen:true op.op_tparams tys f
 
   let is_projection env p =
     try  EcDecl.is_proj (by_path p env)
@@ -2815,7 +2792,7 @@ module Ax = struct
   let instantiate p tys env =
     match by_path_opt p env with
     | Some ({ ax_spec = f } as ax) ->
-        Tvar.f_subst ~freshen:true (List.map fst ax.ax_tparams) tys f
+        Tvar.f_subst ~freshen:true ax.ax_tparams tys f
     | _ -> raise (LookupFailure (`Path p))
 
   let iter ?name f (env : env) =
@@ -2930,20 +2907,6 @@ module Theory = struct
     | Th_theory (x, cth) when cth.cth_mode = `Concrete ->
         bind_instance_th (xpath x) inst cth.cth_items
 
-    | Th_type (x, tyd) -> begin
-        match tyd.tyd_type with
-        | Abstract tc ->
-            let myty =
-              let typ = List.map (fst_map EcIdent.fresh) tyd.tyd_params in
-                (typ, EcTypes.tconstr (xpath x) (List.map (tvar |- fst) typ))
-            in
-              Sp.fold
-                (fun p inst -> TypeClass.bind_instance myty (`General p) inst)
-                tc inst
-
-        | _ -> inst
-    end
-
     | _ -> inst
 
   (* ------------------------------------------------------------------ *)
@@ -2964,17 +2927,6 @@ module Theory = struct
       end
     | _ -> odfl base (tx path base item.ti_item)
 
-  (* ------------------------------------------------------------------ *)
-  let bind_tc_th =
-    let for1 path base = function
-      | Th_typeclass (x, tc) ->
-          tc.tc_prt |> omap (fun prt ->
-            let src = EcPath.pqname path x in
-            TC.Graph.add ~src ~dst:prt base)
-      | _ -> None
-
-    in bind_base_th for1
-
   (* ------------------------------------------------------------------ *)
   let bind_br_th =
     let for1 path base = function
@@ -3047,14 +2999,13 @@ module Theory = struct
       | _, `Concrete ->
           let thname      = EcPath.pqname (root env) cth.name in
           let env_tci     = bind_instance_th thname env.env_tci items in
-          let env_tc      = bind_tc_th thname env.env_tc items in
           let env_rwbase  = bind_br_th thname env.env_rwbase items in
           let env_atbase  = bind_at_th thname env.env_atbase items in
           let env_ntbase  = bind_nt_th thname env.env_ntbase items in
           let env_redbase = bind_rd_th thname env.env_redbase items in
           let env =
             { env with
-                env_tci   ; env_tc     ; env_rwbase;
+                env_tci   ; env_rwbase;
                 env_atbase; env_ntbase; env_redbase; }
           in
           add_restr_th thname env items
@@ -3106,9 +3057,6 @@ module Theory = struct
         | Th_theory (x, ({cth_mode = `Abstract} as th)) ->
             MC.import_theory (xpath x) th env
 
-        | Th_typeclass (x, tc) ->
-            MC.import_typeclass (xpath x) tc env
-
         | Th_baserw (x, _) ->
             MC.import_rwbase (xpath x) env
 
@@ -3265,7 +3213,6 @@ module Theory = struct
     | `Concrete ->
       { env with
           env_tci     = bind_instance_th thpath env.env_tci cth.cth_items;
-          env_tc      = bind_tc_th thpath env.env_tc cth.cth_items;
           env_rwbase  = bind_br_th thpath env.env_rwbase cth.cth_items;
           env_atbase  = bind_at_th thpath env.env_atbase cth.cth_items;
           env_ntbase  = bind_nt_th thpath env.env_ntbase cth.cth_items;

src/ecEnv.mli

@@ -380,7 +380,6 @@ module TypeClass : sig
   type t = typeclass
 
   val add   : path -> env -> env
-  val bind  : ?import:bool -> symbol -> t -> env -> env
   val graph : env -> EcTypeClass.graph
 
   val by_path     : path -> env -> t

src/ecHiGoal.ml

@@ -490,7 +490,7 @@ let process_exacttype qs (tc : tcenv1) =
       tc_error !!tc "%a" EcEnv.pp_lookup_failure cause
   in
   let tys =
-    List.map (fun (a,_) -> EcTypes.tvar a)
+    List.map (fun a -> EcTypes.tvar a)
       (EcEnv.LDecl.tohyps hyps).h_tvar in
   let pt = ptglobal ~tys p in
 
@@ -700,7 +700,7 @@ let process_delta ~und_delta ?target (s, o, p) tc =
             match sform_of_form fp with
             | SFop ((_, tvi), []) -> begin
               (* FIXME: TC HOOK *)
-              let body  = Tvar.f_subst ~freshen:true (List.map fst tparams) tvi body in
+              let body  = Tvar.f_subst ~freshen:true tparams tvi body in
               let body  = f_app body args topfp.f_ty in
                 try  EcReduction.h_red EcReduction.beta_red hyps body
                 with EcEnv.NotReducible -> body
@@ -723,7 +723,7 @@ let process_delta ~und_delta ?target (s, o, p) tc =
   | `RtoL ->
     let fp =
       (* FIXME: TC HOOK *)
-      let body  = Tvar.f_subst ~freshen:true (List.map fst tparams) tvi body in
+      let body  = Tvar.f_subst ~freshen:true tparams tvi body in
       let fp    = f_app body args p.f_ty in
         try  EcReduction.h_red EcReduction.beta_red hyps fp
         with EcEnv.NotReducible -> fp