Merge branch 'trunk' into pr379

1 files changed, 414 insertions, 0 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
new file mode 100644
index 000000000..415b98f2d
--- /dev/null
+++ b/vernac/classes.ml
@@ -0,0 +1,414 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i*)
+open Names
+open Term
+open Vars
+open Environ
+open Nametab
+open CErrors
+open Util
+open Typeclasses_errors
+open Typeclasses
+open Libnames
+open Globnames
+open Constrintern
+open Constrexpr
+open Sigma.Notations
+open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
+(*i*)
+
+open Decl_kinds
+open Entries
+
+let refine_instance = ref true
+
+let _ = Goptions.declare_bool_option {
+  Goptions.optsync  = true;
+  Goptions.optdepr  = false;
+  Goptions.optname  = "definition of instances by refining";
+  Goptions.optkey   = ["Refine";"Instance";"Mode"];
+  Goptions.optread  = (fun () -> !refine_instance);
+  Goptions.optwrite = (fun b -> refine_instance := b)
+}
+
+let typeclasses_db = "typeclass_instances"
+
+let set_typeclass_transparency c local b = 
+  Hints.add_hints local [typeclasses_db] 
+    (Hints.HintsTransparencyEntry ([c], b))
+    
+let _ =
+  Hook.set Typeclasses.add_instance_hint_hook
+    (fun inst path local info poly ->
+     let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)
+       | IsGlobal gr -> Hints.IsGlobRef gr
+     in
+     let info =
+       let open Vernacexpr in
+       { info with hint_pattern =
+		   Option.map
+		     (Constrintern.intern_constr_pattern (Global.env()))
+		     info.hint_pattern } in
+     Flags.silently (fun () ->
+	Hints.add_hints local [typeclasses_db]
+	  (Hints.HintsResolveEntry
+	     [info, poly, false, Hints.PathHints path, inst'])) ());
+  Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
+  Hook.set Typeclasses.classes_transparent_state_hook
+    (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db))
+
+open Vernacexpr
+
+(** TODO: add subinstances *)
+let existing_instance glob g info =
+  let c = global g in
+  let info = Option.default Hints.empty_hint_info info in
+  let instance = Global.type_of_global_unsafe c in
+  let _, r = decompose_prod_assum instance in
+    match class_of_constr Evd.empty (EConstr.of_constr r) with
+      | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob
+  (*FIXME*) (Flags.use_polymorphic_flag ()) c)
+      | None -> user_err ~loc:(loc_of_reference g)
+                         ~hdr:"declare_instance"
+                         (Pp.str "Constant does not build instances of a declared type class.")
+
+let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
+let mismatched_props env n m = mismatched_ctx_inst env Properties n m
+
+(* Declare everything in the parameters as implicit, and the class instance as well *)
+
+let type_ctx_instance evars env ctx inst subst =
+  let rec aux (subst, instctx) l = function
+    decl :: ctx ->
+      let t' = substl subst (RelDecl.get_type decl) in
+      let c', l =
+	match decl with
+	| LocalAssum _ -> EConstr.Unsafe.to_constr (interp_casted_constr_evars env evars (List.hd l) t'), List.tl l
+	| LocalDef (_,b,_) -> substl subst b, l
+      in
+      let d = RelDecl.get_name decl, Some c', t' in
+	aux (c' :: subst, d :: instctx) l ctx
+    | [] -> subst
+  in aux (subst, []) inst (List.rev ctx)
+
+let id_of_class cl =
+  match cl.cl_impl with
+    | ConstRef kn -> let _,_,l = repr_con kn in Label.to_id l
+    | IndRef (kn,i) ->
+	let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in
+	  mip.(0).Declarations.mind_typename
+    | _ -> assert false
+
+open Pp
+
+let instance_hook k info global imps ?hook cst =
+  Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
+  Typeclasses.declare_instance (Some info) (not global) cst;
+  (match hook with Some h -> h cst | None -> ())
+
+let declare_instance_constant k info global imps ?hook id pl poly evm term termtype =
+  let kind = IsDefinition Instance in
+  let evm = 
+    let levels = Univ.LSet.union (Universes.universes_of_constr termtype) 
+				 (Universes.universes_of_constr term) in
+    Evd.restrict_universe_context evm levels 
+  in
+  let pl, uctx = Evd.universe_context ?names:pl evm in
+  let entry = 
+    Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
+  in
+  let cdecl = (DefinitionEntry entry, kind) in
+  let kn = Declare.declare_constant id cdecl in
+    Declare.definition_message id;
+    Universes.register_universe_binders (ConstRef kn) pl;
+    instance_hook k info global imps ?hook (ConstRef kn);
+    id
+
+let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props
+    ?(generalize=true)
+    ?(tac:unit Proofview.tactic option) ?hook pri =
+  let env = Global.env() in
+  let ((loc, instid), pl) = instid in
+  let uctx = Evd.make_evar_universe_context env pl in
+  let evars = ref (Evd.from_ctx uctx) in
+  let tclass, ids =
+    match bk with
+    | Decl_kinds.Implicit ->
+	Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
+	  (fun avoid (clname, _) ->
+	    match clname with
+	    | Some (cl, b) ->
+		let t = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
+		  t, avoid
+	    | None -> failwith ("new instance: under-applied typeclass"))
+	  cl
+    | Explicit -> cl, Id.Set.empty
+  in
+  let tclass = 
+    if generalize then CGeneralization (Loc.ghost, Implicit, Some AbsPi, tclass) 
+    else tclass 
+  in
+  let k, u, cty, ctx', ctx, len, imps, subst =
+    let impls, ((env', ctx), imps) = interp_context_evars env evars ctx in
+    let ctx = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) ctx in
+    let c', imps' = interp_type_evars_impls ~impls env' evars tclass in
+    let c' = EConstr.Unsafe.to_constr c' in
+    let len = List.length ctx in
+    let imps = imps @ Impargs.lift_implicits len imps' in
+    let ctx', c = decompose_prod_assum c' in
+    let ctx'' = ctx' @ ctx in
+    let k, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in
+    let cl, u = Typeclasses.typeclass_univ_instance k in
+    let _, args = 
+      List.fold_right (fun decl (args, args') ->
+	match decl with
+	| LocalAssum _ -> (List.tl args, List.hd args :: args')
+	| LocalDef (_,b,_) -> (args, substl args' b :: args'))
+	(snd cl.cl_context) (args, [])
+    in
+      cl, u, c', ctx', ctx, len, imps, args
+  in
+  let id =
+    match instid with
+	Name id ->
+	  let sp = Lib.make_path id in
+	    if Nametab.exists_cci sp then
+	      user_err ~hdr:"new_instance" (Nameops.pr_id id ++ Pp.str " already exists.");
+	    id
+      | Anonymous ->
+	  let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
+	    Namegen.next_global_ident_away i (Termops.ids_of_context env)
+  in
+  let env' = push_rel_context ctx env in
+  evars := Evarutil.nf_evar_map !evars;
+  evars := resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env !evars;
+  let subst = List.map (fun c -> EConstr.Unsafe.to_constr (Evarutil.nf_evar !evars (EConstr.of_constr c))) subst in
+    if abstract then
+      begin
+	let subst = List.fold_left2
+	  (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
+	  [] subst (snd k.cl_context)
+	in
+	let (_, ty_constr) = instance_constructor (k,u) subst in
+	let nf, subst = Evarutil.e_nf_evars_and_universes evars in
+	let termtype =
+	  let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
+	    nf t
+	in
+	Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
+	let pl, ctx = Evd.universe_context ?names:pl !evars in
+	let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
+	  (ParameterEntry 
+            (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
+	in
+	  Universes.register_universe_binders (ConstRef cst) pl;
+	  instance_hook k pri global imps ?hook (ConstRef cst); id
+      end
+    else (
+      let props =
+	match props with
+	| Some (true, CRecord (loc, fs)) ->
+	    if List.length fs > List.length k.cl_props then
+	      mismatched_props env' (List.map snd fs) k.cl_props;
+	    Some (Inl fs)
+	| Some (_, t) -> Some (Inr t)
+	| None -> 
+	    if Flags.is_program_mode () then Some (Inl [])
+	    else None
+      in
+      let subst =
+	match props with
+	| None -> if List.is_empty k.cl_props then Some (Inl subst) else None
+	| Some (Inr term) ->
+	    let c = interp_casted_constr_evars env' evars term cty in
+	    let c = EConstr.Unsafe.to_constr c in
+	      Some (Inr (c, subst))
+	| Some (Inl props) ->
+	    let get_id =
+	      function
+		| Ident id' -> id'
+		| Qualid (loc,id') -> (loc, snd (repr_qualid id'))
+	    in
+	    let props, rest =
+	      List.fold_left
+		(fun (props, rest) decl ->
+		  if is_local_assum decl then
+		    try
+		      let is_id (id', _) = match RelDecl.get_name decl, get_id id' with
+			| Name id, (_, id') -> Id.equal id id'
+			| Anonymous, _ -> false
+                      in
+		       let (loc_mid, c) =
+			 List.find is_id rest 
+		       in
+		       let rest' = 
+			 List.filter (fun v -> not (is_id v)) rest 
+		       in
+		       let (loc, mid) = get_id loc_mid in
+			 List.iter (fun (n, _, x) -> 
+				      if Name.equal n (Name mid) then
+					Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x)
+			   k.cl_projs;
+			 c :: props, rest'
+		     with Not_found ->
+		       (CHole (Loc.ghost, None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None) :: props), rest
+		   else props, rest)
+		([], props) k.cl_props
+	    in
+              match rest with
+              | (n, _) :: _ ->
+		unbound_method env' k.cl_impl (get_id n)
+              | _ ->
+		Some (Inl (type_ctx_instance evars (push_rel_context ctx' env') 
+			     k.cl_props props subst))
+      in	  
+      let term, termtype =
+	match subst with
+	| None -> let termtype = it_mkProd_or_LetIn cty ctx in
+	    None, termtype
+	| Some (Inl subst) ->
+	  let subst = List.fold_left2
+	    (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
+	    [] subst (k.cl_props @ snd k.cl_context)
+	  in
+	  let (app, ty_constr) = instance_constructor (k,u) subst in
+	  let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
+	  let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
+	    Some term, termtype
+	| Some (Inr (def, subst)) ->
+	  let termtype = it_mkProd_or_LetIn cty ctx in
+	  let term = Termops.it_mkLambda_or_LetIn def ctx in
+	    Some term, termtype
+      in
+      let _ = 
+	evars := Evarutil.nf_evar_map !evars;
+	evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true
+          env !evars;
+	(* Try resolving fields that are typeclasses automatically. *)
+	evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false
+	  env !evars
+      in
+      let _ = evars := Evarutil.nf_evar_map_undefined !evars in
+      let evm, nf = Evarutil.nf_evar_map_universes !evars in
+      let termtype = nf termtype in
+      let _ = (* Check that the type is free of evars now. *)
+	Pretyping.check_evars env Evd.empty evm (EConstr.of_constr termtype)
+      in
+      let term = Option.map nf term in
+	if not (Evd.has_undefined evm) && not (Option.is_empty term) then
+	  declare_instance_constant k pri global imps ?hook id pl
+            poly evm (Option.get term) termtype
+	else if Flags.is_program_mode () || refine || Option.is_empty term then begin
+	  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+	    if Flags.is_program_mode () then
+	      let hook vis gr _ =
+		let cst = match gr with ConstRef kn -> kn | _ -> assert false in
+		  Impargs.declare_manual_implicits false gr ~enriching:false [imps];
+		  Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
+	      in
+	      let obls, constr, typ =
+		match term with 
+		| Some t -> 
+		  let obls, _, constr, typ = 
+		    Obligations.eterm_obligations env id evm 0 t termtype
+		  in obls, Some constr, typ
+		| None -> [||], None, termtype
+	      in
+              let hook = Lemmas.mk_hook hook in
+	      let ctx = Evd.evar_universe_context evm in
+		ignore (Obligations.add_definition id ?term:constr
+ 			?pl typ ctx ~kind:(Global,poly,Instance) ~hook obls);
+		id
+	    else
+	      (Flags.silently 
+	       (fun () ->
+                  (* spiwack: it is hard to reorder the actions to do
+                     the pretyping after the proof has opened. As a
+                     consequence, we use the low-level primitives to code
+                     the refinement manually.*)
+		let gls = List.rev (Evd.future_goals evm) in
+                let evm = Evd.reset_future_goals evm in
+                Lemmas.start_proof id kind evm (EConstr.of_constr termtype)
+		(Lemmas.mk_hook
+                  (fun _ -> instance_hook k pri global imps ?hook));
+                 (* spiwack: I don't know what to do with the status here. *)
+		if not (Option.is_empty term) then
+                  let init_refine =
+                    Tacticals.New.tclTHENLIST [
+                      Refine.refine { run = fun evm -> Sigma (EConstr.of_constr (Option.get term), evm, Sigma.refl) };
+                      Proofview.Unsafe.tclNEWGOALS gls;
+                      Tactics.New.reduce_after_refine;
+                    ]
+                  in
+		  ignore (Pfedit.by init_refine)
+		else if Flags.is_auto_intros () then
+		  ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro));
+		(match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ();
+	       id)
+	end
+      else CErrors.error "Unsolved obligations remaining.")
+	
+let named_of_rel_context l =
+  let acc, ctx =
+    List.fold_right
+      (fun decl (subst, ctx) ->
+        let id = match RelDecl.get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
+	let d = match decl with
+	  | LocalAssum (_,t) -> id, None, substl subst t
+	  | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
+	  (mkVar id :: subst, d :: ctx))
+      l ([], [])
+  in ctx
+
+let context poly l =
+  let env = Global.env() in
+  let evars = ref (Evd.from_env env) in
+  let _, ((env', fullctx), impls) = interp_context_evars env evars l in
+  let fullctx = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) fullctx in
+  let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in
+  let fullctx = Context.Rel.map subst fullctx in
+  let ce t = Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr t) in
+  let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
+  let ctx =
+    try named_of_rel_context fullctx
+    with e when CErrors.noncritical e ->
+      error "Anonymous variables not allowed in contexts."
+  in
+  let uctx = ref (Evd.universe_context_set !evars) in
+  let fn status (id, b, t) =
+    if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
+      let ctx = Univ.ContextSet.to_context !uctx in
+      (* Declare the universe context once *)
+      let () = uctx := Univ.ContextSet.empty in
+      let decl = (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) in
+      let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
+	match class_of_constr !evars (EConstr.of_constr t) with
+	| Some (rels, ((tc,_), args) as _cl) ->
+	    add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (*FIXME*)
+			    poly (ConstRef cst));
+            status
+	    (* declare_subclasses (ConstRef cst) cl *)
+	| None -> status
+    else
+      let test (x, _) = match x with
+      | ExplByPos (_, Some id') -> Id.equal id id'
+      | _ -> false
+      in
+      let impl = List.exists test impls in
+      let decl = (Discharge, poly, Definitional) in
+      let nstatus =
+        pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl
+          Vernacexpr.NoInline (Loc.ghost, id))
+      in
+      let () = uctx := Univ.ContextSet.empty in
+	status && nstatus
+  in List.fold_left fn true (List.rev ctx)