Quelle ring.ml Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

module CVars = Vars
open Ltac_plugin
open Pp
open Util
open Names
open Constr
open EConstr
open Vars
open Environ
open Glob_term
open Locus
open Tacexpr
open Rocqlib
open Mod_subst
open Tacinterp
open Libobject
open Printer
open Declare
open Ring_ast
open Proofview.Notations

let error msg = CErrors.user_err Pp.(str msg)

(****************************************************************************)
(* controlled reduction *)

type protect_flag = Eval|Prot|Rec
type 'a reduction = Full | Arg of 'a

type protection = {
  with_eq : bool;
  arguments : ((unit -> GlobRef.t) * (int -> protect_flag) reduction) list;
}

type rprotection = {
  r_with_eq : bool;
  r_arguments : (GlobRef.t * (int -> protect_flag) reduction) list;
}

let interp_map env sigma l c = match EConstr.destRef sigma c with
| exception DestKO-> None
| (t, _) ->
  let eq g1 g2 = QGlobRef.equal env g1 g2 in
  match List.assoc_f eq t l.r_arguments with
  | exception Not_found -> None
  | Full -> Some Full
  | Arg f -> Some (Arg f)

let fresh_rel (n, data) c =
  let n = n + 1 in
  (n, c :: data), mkRel n

let rec mk_clos_but env sigma f_map accu t =
  let (f, args) = EConstr.decompose_app sigma t in
  match interp_map env sigma f_map f with
  | Some Full -> (accu, t)
  | Some (Arg tag) ->
    let fold i accu t = tag_arg env sigma f_map accu (tag i) t in
    if Array.is_empty args then (accu, t)
    else
      let (accu, args) = Array.fold_left_map_i fold accu args in
      accu, mkApp (f, args)
  | None -> fresh_rel accu t

and tag_arg env sigma f_map accu tag c = match tag with
| Eval -> accu, c
| Prot -> fresh_rel accu c
| Rec -> mk_clos_but env sigma f_map accu c

let protect_maps : protection String.Map.t ref = ref String.Map.empty
let add_map s m = protect_maps := String.Map.add s m !protect_maps

let dest_rel sigma t =
  match EConstr.kind sigma t with
  | App(f,args) when Array.length args >= 2 ->
      let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in
      if closed0 sigma rel then
        (rel,args.(Array.length args - 2),args.(Array.length args - 1))
      else error "ring: cannot find relation (not closed)"
  | _ -> error "ring: cannot find relation"

let lookup_map map =
  let map = match String.Map.find_opt map !protect_maps with
  | Some map -> map
  | None -> CErrors.user_err (str "Map " ++ qs map ++ str "not found.")
  in
  let r_arguments = List.map (fun (c, map) -> (c (), map)) map.arguments in
  let r_with_eq = map.with_eq in
  { r_with_eq; r_arguments }

let protect_red map env sigma c =
  let map = lookup_map map in
  let rec eval n c = match EConstr.kind sigma c with
  | Prod (na, t, u) -> EConstr.mkProd (na, eval n t, eval (n + 1) u)
  | _ ->
    let rels = List.init n (fun i -> mkRel (n - i)) in
    let norm c =
      let (_, subterms), c = mk_clos_but env sigma map (n, rels) c in
      let c = Reductionops.clos_norm_flags RedFlags.all env sigma c in
      let subst = List.rev subterms in
      EConstr.Vars.substl subst c
    in
    if map.r_with_eq then
      let (rel, a1, a2) = dest_rel sigma c in
      mkApp (rel, [|norm a1; norm a2|])
    else
      norm c
  in
  eval 0 c

let protect_tac map =
  Tactics.reduct_option ~check:false (protect_red map,DEFAULTcast) None

let protect_tac_in map id =
  Tactics.reduct_option ~check:false (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp))

(****************************************************************************)

let rec closed_under sigma cset t =
  try
    let (gr, _) = destRef sigma t in
    GlobRef.Set_env.mem gr cset
  with DestKO ->
    match EConstr.kind sigma t with
    | Cast(c,_,_) -> closed_under sigma cset c
    | App(f,l) -> closed_under sigma cset f && Array.for_all (closed_under sigma cset) l
    | _ -> false

let closed_term args _ = match args with
| [t; l] ->
  let t = Option.get (Value.to_constr t) in
  let l = List.map (fun c -> Value.cast (Genarg.topwit Stdarg.wit_ref) c) (Option.get (Value.to_list l)) in
  Proofview.tclEVARMAP >>= fun sigma ->
  let cs = List.fold_right GlobRef.Set_env.add l GlobRef.Set_env.empty in
  if closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.tclFAIL (mt())
| _ -> assert false

let closed_term_ast =
  let tacname = {
    mltac_plugin = "rocq-runtime.plugins.ring";
    mltac_tactic = "closed_term";
  } in
  let () = Tacenv.register_ml_tactic tacname [|closed_term|] in
  let tacname = {
    mltac_name = tacname;
    mltac_index = 0;
  } in
  fun l ->
  let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in
  CAst.make (TacFun
    ([Name(Id.of_string"t")],
    CAst.make (TacML (tacname,
    [TacGeneric (None, Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None));
     TacGeneric (None, Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))))
(*
let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
*)

(****************************************************************************)

let ic env sigma c =
  let c, uctx = Constrintern.interp_constr env sigma c in
  (Evd.from_ctx uctx, c)

let ic_unsafe env sigma c = (*FIXME remove *)
  fst (Constrintern.interp_constr env sigma c)

let decl_constant name univs c =
  let open Constr in
  let vars = CVars.universes_of_constr c in
  let univs = UState.restrict_universe_context univs vars in
  let () = Global.push_context_set univs in
  let types = (Typeops.infer (Global.env ()) c).uj_type in
  let univs = UState.Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders in
  (* UnsafeMonomorphic: we always do poly:false *)
  UnsafeMonomorphic.mkConst
    (declare_constant ~name
       ~kind:Decls.(IsProof Lemma)
       (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c)))

let decl_constant na suff univs c =
  let na = Namegen.next_global_ident_away (Global.safe_env ()) (Nameops.add_suffix na suff) Id.Set.empty in
  decl_constant na univs c

(* Calling a global tactic *)
let ltac_call tac (args:glob_tactic_arg list) =
  CAst.make @@ TacArg (TacCall (CAst.make (ArgArg(Loc.tag @@ Lazy.force tac),args)))

let constr_of sigma v = match Value.to_constr v with
  | Some c -> EConstr.to_constr sigma c
  | None -> failwith "Ring.exec_tactic: anomaly"

let tactic_res = ref [||]

let get_res =
  let open Tacexpr in
  let name = { mltac_plugin = "rocq-runtime.plugins.ring"; mltac_tactic = "get_res"; } in
  let entry = { mltac_name = name; mltac_index = 0 } in
  let tac args ist =
    let n = Tacinterp.Value.cast (Genarg.topwit Stdarg.wit_int) (List.hd args) in
    let init i = Id.Map.find (Id.of_string ("x" ^ string_of_int i)) ist.lfun in
    tactic_res := Array.init n init;
    Proofview.tclUNIT ()
  in
  Tacenv.register_ml_tactic name [| tac |];
  entry

let exec_tactic env sigma n f args =
  let fold arg (i, vars, lfun) =
    let id = Id.of_string ("x" ^ string_of_int i) in
    let x = Reference (ArgVar CAst.(make id)) in
    (succ i, x :: vars, Id.Map.add id (Value.of_constr arg) lfun)
  in
  let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
  let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in
  (* Build the getter *)
  let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
  let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in
  let get_res = CAst.make (TacML (get_res, [TacGeneric (None, n)])) in
  let getter = Tacexp (CAst.make (TacFun (List.map (fun n -> Name n) lid, get_res))) in
  (* Evaluate the whole result *)
  let _, pv = Proofview.init sigma [env, EConstr.mkProp] in
  let tac = Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter])) in
  let ((), pv, _, _, _) = Proofview.apply ~name:(Id.of_string "ring") ~poly:false (Global.env ()) tac pv in
  let sigma = Evd.minimize_universes (Proofview.return pv) in
  let nf c = constr_of sigma c in
  Array.map nf !tactic_res, Evd.universe_context_set sigma

let gen_constant n = (); fun () -> (EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Global.env ()) (Rocqlib.lib_ref n)))
let gen_reference n = (); fun () -> (Rocqlib.lib_ref n)

let rocq_mk_Setoid = gen_constant "plugins.ring.Build_Setoid_Theory"
let rocq_None = gen_reference "core.option.None"
let rocq_Some = gen_reference "core.option.Some"
let rocq_eq = gen_reference "core.eq.type"

let rocq_cons = gen_reference "core.list.cons"
let rocq_nil = gen_reference "core.list.nil"

let lapp f args = mkApp (f (), args)

let plapp sigma f args =
  let sigma, fc = Evd.fresh_global (Global.env ()) sigma (f ()) in
  sigma, mkApp(fc,args)

(****************************************************************************)
(* Library linking *)

let plugin_dir = "setoid_ring"

let cdir = ["Stdlib";plugin_dir]

let znew_ring_path =
  DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Stdlib"])
let zltac s =
  lazy(KerName.make (ModPath.MPfile znew_ring_path) (Label.make s))

(* Ring theory *)

(* almost_ring defs *)
let rocq_almost_ring_theory = gen_reference "plugins.ring.almost_ring_theory"

(* setoid and morphism utilities *)
let rocq_eq_setoid = gen_reference "plugins.ring.Eqsth"
let rocq_eq_morph = gen_reference "plugins.ring.Eq_ext"
let rocq_eq_smorph = gen_reference "plugins.ring.Eq_s_ext"

(* ring -> almost_ring utilities *)
let rocq_ring_theory = gen_reference "plugins.ring.ring_theory"
let rocq_mk_reqe = gen_constant "plugins.ring.mk_reqe"

(* semi_ring -> almost_ring utilities *)
let rocq_semi_ring_theory = gen_reference "plugins.ring.semi_ring_theory"
let rocq_mk_seqe = gen_constant "plugins.ring.mk_seqe"

let rocq_abstract = gen_constant "plugins.ring.Abstract"
let rocq_comp = gen_constant "plugins.ring.Computational"
let rocq_morph = gen_constant "plugins.ring.Morphism"

(* power function *)
let ltac_inv_morph_nothing = zltac"inv_morph_nothing"

(* hypothesis *)
let rocq_mkhypo = gen_reference "plugins.ring.mkhypo"
let rocq_hypo = gen_reference "plugins.ring.hypo"

(* Equality: do not evaluate but make recursive call on both sides *)
let map_with_eq arg_map =
  { with_eq = true; arguments = arg_map }

let map_without_eq arg_map =
  { with_eq = false; arguments = arg_map }

let base_red = [
  rocq_cons, Arg (function 2->Rec|_->Prot);
  rocq_nil, Arg (function _ -> Prot);
  gen_reference "plugins.ring.IDphi", Full;
  gen_reference "plugins.ring.gen_phiZ", Full;
]

let ring_red = [
  (* Pphi_dev: evaluate polynomial and coef operations, protect
      ring operations and make recursive call on the var map *)
  gen_reference "plugins.ring.Pphi_dev", Arg (function 8|9|10|12|14->Eval|11|13->Rec|_->Prot);
  gen_reference "plugins.ring.Pphi_pow",
        Arg (function 8|9|10|13|15|17->Eval|11|16->Rec|_->Prot);
  (* PEeval: evaluate polynomial, protect ring
      operations and make recursive call on the var map *)
  gen_reference "plugins.ring.eval", Arg (function 10|13->Eval|8|12->Rec|_->Prot)
]

let _ = add_map "ring"
  (map_with_eq
    @@
    base_red @
    ring_red)

(****************************************************************************)
(* Ring database *)

module Cmap = Map.Make(Constr)

let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"

let print_rings () =
  Feedback.msg_notice (strbrk "The following ring structures have been declared:");
  Cmap.iter (fun _carrier ring ->
      let env = Global.env () in
      let sigma = Evd.from_env env in
      Feedback.msg_notice
        (hov 2
           (Ppconstr.pr_id ring.ring_name ++ spc() ++
            str"with carrier "++ pr_constr_env env sigma ring.ring_carrier++spc()++
            str"and equivalence relation "++ pr_constr_env env sigma ring.ring_req))
    ) !from_carrier

let ring_for_carrier r = Cmap.find r !from_carrier

let find_ring_structure env sigma l =
  match l with
    | t::cl' ->
        let ty = Retyping.get_type_of env sigma t in
        let check c =
          let ty' = Retyping.get_type_of env sigma c in
          if not (Reductionops.is_conv env sigma ty ty') then
            CErrors.user_err
              (str"Arguments of ring_simplify do not have all the same type.")
        in
        List.iter check cl';
        (try ring_for_carrier (EConstr.to_constr ~abort_on_undefined_evars:false sigma ty)
        with Not_found ->
          CErrors.user_err
            (str"Cannot find a declared ring structure over"++
             spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\"."))
    | [] -> assert false

let add_entry e =
  from_carrier := Cmap.add e.ring_carrier e !from_carrier

let subst_th (subst,th) =
  let c' = subst_mps subst th.ring_carrier in
  let eq' = subst_mps subst th.ring_req in
  let set' = subst_mps subst th.ring_setoid in
  let ext' = subst_mps subst th.ring_ext in
  let morph' = subst_mps subst th.ring_morph in
  let th' = subst_mps subst th.ring_th in
  let thm1' = subst_mps subst th.ring_lemma1 in
  let thm2' = subst_mps subst th.ring_lemma2 in
  let tac'= Tacsubst.subst_tactic subst th.ring_cst_tac in
  let pow_tac'= Tacsubst.subst_tactic subst th.ring_pow_tac in
  let pretac'= Tacsubst.subst_tactic subst th.ring_pre_tac in
  let posttac'= Tacsubst.subst_tactic subst th.ring_post_tac in
  if c' == th.ring_carrier &&
     eq' == th.ring_req &&
     Constr.equal set' th.ring_setoid &&
     ext' == th.ring_ext &&
     morph' == th.ring_morph &&
     th' == th.ring_th &&
     thm1' == th.ring_lemma1 &&
     thm2' == th.ring_lemma2 &&
     tac' == th.ring_cst_tac &&
     pow_tac' == th.ring_pow_tac &&
     pretac' == th.ring_pre_tac &&
     posttac' == th.ring_post_tac then th
  else
    { ring_name = th.ring_name;
      ring_carrier = c';
      ring_req = eq';
      ring_setoid = set';
      ring_ext = ext';
      ring_morph = morph';
      ring_th = th';
      ring_cst_tac = tac';
      ring_pow_tac = pow_tac';
      ring_lemma1 = thm1';
      ring_lemma2 = thm2';
      ring_pre_tac = pretac';
      ring_post_tac = posttac' }

let theory_to_obj : ring_info -> obj =
  declare_object @@ global_object_nodischarge "tactic-new-ring-theory"
    ~cache:add_entry
    ~subst:(Some subst_th)

let setoid_of_relation env sigma a r =
  try
    let sigma, refl = Rewrite.get_reflexive_proof env sigma a r in
    let sigma, sym = Rewrite.get_symmetric_proof env sigma a r in
    let sigma, trans = Rewrite.get_transitive_proof env sigma a r in
    sigma, lapp rocq_mk_Setoid [|a ; r ; refl; sym; trans |]
  with Not_found ->
    CErrors.user_err (str "Cannot find a setoid structure for relation " ++ pr_econstr_env env sigma r ++ str ".")

let op_morph r add mul opp req m1 m2 m3 =
  lapp rocq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |]

let op_smorph r add mul req m1 m2 =
  lapp rocq_mk_seqe [| r; add; mul; req; m1; m2 |]

let ring_equality env sigma (r,add,mul,opp,req) =
  match EConstr.kind sigma req with
  | App (f, [| _ |]) when isRefX env sigma (rocq_eq ()) f ->
    let sigma, setoid = plapp sigma rocq_eq_setoid [|r|] in
    let sigma, op_morph =
      match opp with
        Some opp -> plapp sigma rocq_eq_morph [|r;add;mul;opp|]
      | None -> plapp sigma rocq_eq_smorph [|r;add;mul|] in
    let sigma, setoid = Typing.solve_evars env sigma setoid in
    let sigma, op_morph = Typing.solve_evars env sigma op_morph in
    (sigma,setoid,op_morph)
  | _ ->
    let sigma, setoid = setoid_of_relation env sigma r req in
    let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in
    let sigma, add_m, add_m_lem =
      try Rewrite.Internal.default_morphism env sigma signature add
      with Not_found ->
        CErrors.user_err (str "Ring addition " ++ pr_econstr_env env sigma add ++ str " should be declared as a morphism.") in
    let sigma, mul_m, mul_m_lem =
      try Rewrite.Internal.default_morphism env sigma signature mul
      with Not_found ->
        CErrors.user_err (str "Ring multiplication " ++ pr_econstr_env env sigma mul ++ str " should be declared as a morphism.") in
    let sigma, op_morph =
      match opp with
      | Some opp ->
        (let sigma, opp_m,opp_m_lem =
           try Rewrite.Internal.default_morphism env sigma ([Some(r,Some req)],Some(r,Some req)) opp
           with Not_found ->
             CErrors.user_err (str "Ring opposite " ++ pr_econstr_env env sigma opp ++ str " should be declared as a morphism.") in
         let op_morph =
           op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
         Flags.if_verbose
           Feedback.msg_info
           (str"Using setoid \""++ pr_econstr_env env sigma req++str"\""++spc()++
            str"and morphisms \""++pr_econstr_env env sigma add_m ++
            str"\","++spc()++ str"\""++pr_econstr_env env sigma mul_m++
            str"\""++spc()++str"and \""++pr_econstr_env env sigma opp_m++
            str"\"");
         sigma, op_morph)
      | None ->
        (Flags.if_verbose
           Feedback.msg_info
           (str"Using setoid \""++pr_econstr_env env sigma req ++str"\"" ++ spc() ++
            str"and morphisms \""++pr_econstr_env env sigma add_m ++
            str"\""++spc()++str"and \""++
            pr_econstr_env env sigma mul_m++str"\"");
         sigma, op_smorph r add mul req add_m_lem mul_m_lem) in
    (sigma,setoid,op_morph)

let build_setoid_params env sigma r add mul opp req eqth =
  match eqth with
      Some (a,b) -> sigma,a,b
    | None -> ring_equality env sigma (r,add,mul,opp,req)

let dest_ring env sigma th_spec =
  let th_typ = Retyping.get_type_of env sigma th_spec in
  match EConstr.kind sigma th_typ with
      App(f,[|r;zero;one;add;mul;sub;opp;req|])
        when isRefX env sigma (rocq_almost_ring_theory ()) f ->
          (None,r,zero,one,add,mul,Some sub,Some opp,req)
    | App(f,[|r;zero;one;add;mul;req|])
        when isRefX env sigma (rocq_semi_ring_theory ()) f ->
        (Some true,r,zero,one,add,mul,None,None,req)
    | App(f,[|r;zero;one;add;mul;sub;opp;req|])
        when isRefX env sigma (rocq_ring_theory ()) f ->
        (Some false,r,zero,one,add,mul,Some sub,Some opp,req)
    | _ -> error "bad ring structure"

let reflect_coeff rkind =
  (* We build an ill-typed terms on purpose... *)
  match rkind with
      Abstract -> rocq_abstract ()
    | Computational c -> lapp rocq_comp [|c|]
    | Morphism m -> lapp rocq_morph [|m|]

let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
  match cst_tac with
      Some (CstTac t) -> Tacintern.glob_tactic t
    | Some (Closed lc) ->
        closed_term_ast (List.map Smartlocate.global_with_alias lc)
    | None ->
        let t = ArgArg(Loc.tag @@ Lazy.force ltac_inv_morph_nothing) in
              CAst.make (TacArg (TacCall (CAst.make (t,[]))))

let make_hyp env sigma c =
  let t = Retyping.get_type_of env sigma c in
  plapp sigma rocq_mkhypo [|t;c|]

let make_hyp_list env sigma lH =
  let sigma, carrier = Evd.fresh_global env sigma (rocq_hypo ()) in
  let sigma, l =
    List.fold_right
      (fun c (sigma,l) ->
        let sigma, c = make_hyp env sigma c in
        plapp sigma rocq_cons [|carrier; c; l|]) lH
        (plapp sigma rocq_nil [|carrier|])
  in
  let sigma, l' = Typing.solve_evars env sigma l in
  sigma, l'

let interp_power env sigma pow =
  let sigma, carrier = Evd.fresh_global env sigma (rocq_hypo ()) in
  match pow with
  | None ->
      let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in
      let sigma, c = plapp sigma rocq_None [|carrier|] in
      sigma, (CAst.make (TacArg (TacCall (CAst.make (t,[])))), c)
  | Some (tac, spec) ->
      let tac =
        match tac with
        | CstTac t -> Tacintern.glob_tactic t
        | Closed lc ->
            closed_term_ast (List.map Smartlocate.global_with_alias lc) in
      let spec = ic_unsafe env sigma spec in
      let sigma, spec = make_hyp env sigma spec in
      let sigma, pow = plapp sigma rocq_Some [|carrier; spec|] in
      sigma, (tac, pow)

let interp_sign env sigma sign =
  let sigma, carrier = Evd.fresh_global env sigma (rocq_hypo ()) in
  match sign with
  | None -> plapp sigma rocq_None [|carrier|]
  | Some spec ->
      let sigma, spec = make_hyp env sigma (ic_unsafe env sigma spec) in
      plapp sigma rocq_Some [|carrier;spec|]
       (* Same remark on ill-typed terms ... *)

let interp_div env sigma div =
  let sigma, carrier = Evd.fresh_global env sigma (rocq_hypo ()) in
  match div with
  | None -> plapp sigma rocq_None [|carrier|]
  | Some spec ->
      let sigma, spec = make_hyp env sigma (ic_unsafe env sigma spec) in
      plapp sigma rocq_Some [|carrier;spec|]
       (* Same remark on ill-typed terms ... *)

let add_theory0 env sigma name rth eqth morphth cst_tac (pre,post) power sign div =
  check_required_library (cdir@["Ring_base"]);
  let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in
  let (sigma, sth,ext) = build_setoid_params env sigma r add mul opp req eqth in
  let sigma, (pow_tac, pspec) = interp_power env sigma power in
  let sigma, sspec = interp_sign env sigma sign in
  let sigma, dspec = interp_div env sigma div in
  let rk = reflect_coeff morphth in
  let params,ctx =
    exec_tactic env sigma 5 (zltac "ring_lemmas")
      [sth;ext;rth;pspec;sspec;dspec;rk] in
  let lemma1 = params.(3) in
  let lemma2 = params.(4) in

  let lemma1 =
    decl_constant name "_ring_lemma1" ctx lemma1 in
  let lemma2 =
    decl_constant name "_ring_lemma2" ctx lemma2 in
  let cst_tac =
    interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
  let pretac =
    match pre with
        Some t -> Tacintern.glob_tactic t
      | _ -> CAst.make (TacId []) in
  let posttac =
    match post with
        Some t -> Tacintern.glob_tactic t
      | _ -> CAst.make (TacId []) in
  let r = EConstr.to_constr sigma r in
  let req = EConstr.to_constr sigma req in
  let sth = EConstr.to_constr sigma sth in
  let _ =
    Lib.add_leaf
      (theory_to_obj
        { ring_name = name;
          ring_carrier = r;
          ring_req = req;
          ring_setoid = sth;
          ring_ext = params.(1);
          ring_morph = params.(2);
          ring_th = params.(0);
          ring_cst_tac = cst_tac;
          ring_pow_tac = pow_tac;
          ring_lemma1 = lemma1;
          ring_lemma2 = lemma2;
          ring_pre_tac = pretac;
          ring_post_tac = posttac }) in
  ()

let ic_coeff_spec env sigma = function
  | Computational t -> Computational (ic_unsafe env sigma t)
  | Morphism t -> Morphism (ic_unsafe env sigma t)
  | Abstract -> Abstract

let set_once s r v =
  if Option.is_empty !r then r := Some v else error (s^" cannot be set twice")

let process_ring_mods env sigma l =
  let kind = ref None in
  let set = ref None in
  let cst_tac = ref None in
  let pre = ref None in
  let post = ref None in
  let sign = ref None in
  let power = ref None in
  let div = ref None in
  List.iter(function
      Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec env sigma k)
    | Const_tac t -> set_once "tactic recognizing constants" cst_tac t
    | Pre_tac t -> set_once "preprocess tactic" pre t
    | Post_tac t -> set_once "postprocess tactic" post t
    | Setoid(sth,ext) -> set_once "setoid" set (ic_unsafe env sigma sth,ic_unsafe env sigma ext)
    | Pow_spec(t,spec) -> set_once "power" power (t,spec)
    | Sign_spec t -> set_once "sign" sign t
    | Div_spec t -> set_once "div" div t) l;
  let k = match !kind with Some k -> k | None -> Abstract in
  (k, !set, !cst_tac, !pre, !post, !power, !sign, !div)

let add_theory id rth l =
  let env = Global.env () in
  let sigma = Evd.from_env env in
  let sigma, rth = ic env sigma rth in
  let (k,set,cst,pre,post,power,sign, div) = process_ring_mods env sigma l in
  add_theory0 env sigma id rth set k cst (pre,post) power sign div

(*****************************************************************************)
(* The tactics consist then only in a lookup in the ring database and
   call the appropriate ltac. *)

let make_args_list sigma rl t =
  match rl with
  | [] -> let (_,t1,t2) = dest_rel sigma t in [t1;t2]
  | _ -> rl

let make_term_list env sigma carrier rl =
  let sigma, l = List.fold_right
    (fun x (sigma,l) -> plapp sigma rocq_cons [|carrier;x;l|]) rl
    (plapp sigma rocq_nil [|carrier|])
  in
  Typing.solve_evars env sigma l

let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c)
let tacarg expr =
  Tacinterp.Value.of_closure (Tacinterp.default_ist ()) expr

let ltac_ring_structure e =
  let req = carg e.ring_req in
  let sth = carg e.ring_setoid in
  let ext = carg e.ring_ext in
  let morph = carg e.ring_morph in
  let th = carg e.ring_th in
  let cst_tac = tacarg e.ring_cst_tac in
  let pow_tac = tacarg e.ring_pow_tac in
  let lemma1 = carg e.ring_lemma1 in
  let lemma2 = carg e.ring_lemma2 in
  let pretac =  tacarg (CAst.make (TacFun ([Anonymous],e.ring_pre_tac))) in
  let posttac = tacarg (CAst.make (TacFun ([Anonymous],e.ring_post_tac))) in
  [req;sth;ext;morph;th;cst_tac;pow_tac;
   lemma1;lemma2;pretac;posttac]

let ring_lookup (f : Value.t) lH rl t =
  Proofview.Goal.enter begin fun gl ->
    let sigma = Tacmach.project gl in
    let env = Proofview.Goal.env gl in
    let rl = make_args_list sigma rl t in
    let e = find_ring_structure env sigma rl in
    let sigma, l = make_term_list env sigma (EConstr.of_constr e.ring_carrier) rl in
    let rl = Value.of_constr l in
    let sigma, l = make_hyp_list env sigma lH in
    let lH = Value.of_constr l in
    let ring = ltac_ring_structure e in
    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Value.apply f (ring@[lH;rl]))
  end

(***********************************************************************)

let new_field_path =
  DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Stdlib"])

let field_ltac s =
  lazy(KerName.make (ModPath.MPfile new_field_path) (Label.make s))

let _ = add_map "field"
  (map_with_eq @@
    base_red @
    ring_red @ [
    (* display_linear: evaluate polynomials and coef operations, protect
       field operations and make recursive call on the var map *)
    gen_reference "plugins.field.display_linear",
      Arg (function 9|10|11|13|15|16->Eval|12|14->Rec|_->Prot);
    gen_reference "plugins.field.display_pow_linear",
     Arg (function 9|10|11|14|16|18|19->Eval|12|17->Rec|_->Prot);
    (* FEeval: evaluate polynomial, protect field
       operations and make recursive call on the var map *)
    gen_reference "plugins.field.FEeval", Arg (function 12|15->Eval|10|14->Rec|_->Prot)]);;

let _ = add_map "field_cond"
  (map_without_eq @@
    base_red @ [
    (* PCond: evaluate denum list, protect ring
       operations and make recursive call on the var map *)
     gen_reference "plugins.field.PCond", Arg (function 11|14->Eval|9|13->Rec|_->Prot)]);;

let _ = Redexpr.declare_reduction "simpl_field_expr"
  (protect_red "field")

let afield_theory = gen_reference "plugins.field.almost_field_theory"
let field_theory = gen_reference "plugins.field.field_theory"
let sfield_theory = gen_reference "plugins.field.semi_field_theory"
let af_ar = gen_reference "plugins.field.AF_AR"
let f_r = gen_reference "plugins.field.F_R"
let sf_sr = gen_reference "plugins.field.SF_SR"
let dest_field env sigma th_spec =
  let th_typ = Retyping.get_type_of env sigma th_spec in
  match EConstr.kind sigma th_typ with
    | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
        when isRefX env sigma (afield_theory ()) f ->
        let sigma, rth = plapp sigma af_ar
          [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
        (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
    | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
        when isRefX env sigma (field_theory ()) f ->
        let sigma, rth =
          plapp sigma f_r
            [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
        (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
    | App(f,[|r;zero;one;add;mul;div;inv;req|])
        when isRefX env sigma (sfield_theory ()) f ->
        let sigma, rth = plapp sigma sf_sr
          [|r;zero;one;add;mul;div;inv;req;th_spec|] in
        (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth)
    | _ -> error "bad field structure"

let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table"

let print_fields () =
  Feedback.msg_notice (strbrk "The following field structures have been declared:");
  Cmap.iter (fun _carrier fi ->
      let env = Global.env () in
      let sigma = Evd.from_env env in
      Feedback.msg_notice
        (hov 2
           (Id.print fi.field_name ++ spc() ++
            str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++
            str"and equivalence relation "++ pr_constr_env env sigma fi.field_req))
    ) !field_from_carrier

let field_for_carrier r = Cmap.find r !field_from_carrier

let find_field_structure env sigma l =
  check_required_library (cdir@["Field_tac"]);
  match l with
    | t::cl' ->
        let ty = Retyping.get_type_of env sigma t in
        let check c =
          let ty' = Retyping.get_type_of env sigma c in
          if not (Reductionops.is_conv env sigma ty ty') then
            CErrors.user_err
              (str"Arguments of field_simplify do not have all the same type.")
        in
        List.iter check cl';
        (try field_for_carrier (EConstr.to_constr sigma ty)
        with Not_found ->
          CErrors.user_err
            (str"Cannot find a declared field structure over"++
             spc()++str"\""++pr_econstr_env env sigma ty++str"\"."))
    | [] -> assert false

let add_field_entry e =
  field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier

let subst_th (subst,th) =
  let c' = subst_mps subst th.field_carrier in
  let eq' = subst_mps subst th.field_req in
  let thm1' = subst_mps subst th.field_ok in
  let thm2' = subst_mps subst th.field_simpl_eq_ok in
  let thm3' = subst_mps subst th.field_simpl_ok in
  let thm4' = subst_mps subst th.field_simpl_eq_in_ok in
  let thm5' = subst_mps subst th.field_cond in
  let tac'= Tacsubst.subst_tactic subst th.field_cst_tac in
  let pow_tac' = Tacsubst.subst_tactic subst th.field_pow_tac in
  let pretac'= Tacsubst.subst_tactic subst th.field_pre_tac in
  let posttac'= Tacsubst.subst_tactic subst th.field_post_tac in
  if c' == th.field_carrier &&
     eq' == th.field_req &&
     thm1' == th.field_ok &&
     thm2' == th.field_simpl_eq_ok &&
     thm3' == th.field_simpl_ok &&
     thm4' == th.field_simpl_eq_in_ok &&
     thm5' == th.field_cond &&
     tac' == th.field_cst_tac &&
     pow_tac' == th.field_pow_tac &&
     pretac' == th.field_pre_tac &&
     posttac' == th.field_post_tac then th
  else
    { field_name = th.field_name;
      field_carrier = c';
      field_req = eq';
      field_cst_tac = tac';
      field_pow_tac = pow_tac';
      field_ok = thm1';
      field_simpl_eq_ok = thm2';
      field_simpl_ok = thm3';
      field_simpl_eq_in_ok = thm4';
      field_cond = thm5';
      field_pre_tac = pretac';
      field_post_tac = posttac' }

let ftheory_to_obj : field_info -> obj =
  declare_object @@ global_object_nodischarge "tactic-new-field-theory"
    ~cache:add_field_entry
    ~subst:(Some subst_th)

let field_equality env sigma r inv req =
  match EConstr.kind sigma req with
  | App (f, [| _ |]) when isRefX env sigma (rocq_eq ()) f ->
    let c = UnivGen.constr_of_monomorphic_global (Global.env ()) Rocqlib.(lib_ref "core.eq.congr") in
    let c = EConstr.of_constr c in
    sigma, mkApp(c,[|r;r;inv|])
  | _ ->
    let _setoid = setoid_of_relation env sigma r req in
    let signature = [Some (r,Some req)],Some(r,Some req) in
    let sigma, inv_m, inv_m_lem =
      try Rewrite.Internal.default_morphism env sigma signature inv
      with Not_found ->
        error "field inverse should be declared as a morphism" in
    sigma, inv_m_lem

let add_field_theory0 env sigma name fth eqth morphth cst_tac inj (pre,post) power sign odiv =
  let open Constr in
  check_required_library (cdir@["Field_tac"]);
  let (sigma,fth) = ic env sigma fth in
  let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) =
    dest_field env sigma fth in
  let (sigma,sth,ext) = build_setoid_params env sigma r add mul opp req eqth in
  let eqth = Some(sth,ext) in
  let _ = add_theory0 env sigma name rth eqth morphth cst_tac (pre,post) power sign odiv in
  let sigma, (pow_tac, pspec) = interp_power env sigma power in
  let sigma, sspec = interp_sign env sigma sign in
  let sigma, dspec = interp_div env sigma odiv in
  let sigma, inv_m = field_equality env sigma r inv req in
  let rk = reflect_coeff morphth in
  let params,ctx =
    exec_tactic env sigma 9 (field_ltac"field_lemmas")
      [sth;ext;inv_m;fth;pspec;sspec;dspec;rk] in
  let lemma1 = params.(3) in
  let lemma2 = params.(4) in
  let lemma3 = params.(5) in
  let lemma4 = params.(6) in
  let cond_lemma =
    match inj with
      | Some thm -> mkApp(params.(8),[|EConstr.to_constr sigma thm|])
      | None -> params.(7) in
  let lemma1 = decl_constant name "_field_lemma1"
    ctx lemma1 in
  let lemma2 = decl_constant name "_field_lemma2"
    ctx lemma2 in
  let lemma3 = decl_constant name "_field_lemma3"
    ctx lemma3 in
  let lemma4 = decl_constant name "_field_lemma4"
    ctx lemma4 in
  let cond_lemma = decl_constant name "_lemma5"
    ctx cond_lemma in
  let cst_tac =
    interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
  let pretac =
    match pre with
        Some t -> Tacintern.glob_tactic t
      | _ -> CAst.make (TacId []) in
  let posttac =
    match post with
        Some t -> Tacintern.glob_tactic t
      | _ -> CAst.make (TacId []) in
  let r = EConstr.to_constr sigma r in
  let req = EConstr.to_constr sigma req in
  let _ =
    Lib.add_leaf
      (ftheory_to_obj
        { field_name = name;
          field_carrier = r;
          field_req = req;
          field_cst_tac = cst_tac;
          field_pow_tac = pow_tac;
          field_ok = lemma1;
          field_simpl_eq_ok = lemma2;
          field_simpl_ok = lemma3;
          field_simpl_eq_in_ok = lemma4;
          field_cond = cond_lemma;
          field_pre_tac = pretac;
          field_post_tac = posttac }) in  ()

let process_field_mods env sigma l =
  let kind = ref None in
  let set = ref None in
  let cst_tac = ref None in
  let pre = ref None in
  let post = ref None in
  let inj = ref None in
  let sign = ref None in
  let power = ref None in
  let div = ref None in
  List.iter(function
      Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec env sigma k)
    | Ring_mod(Const_tac t) ->
        set_once "tactic recognizing constants" cst_tac t
    | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t
    | Ring_mod(Post_tac t) -> set_once "postprocess tactic" post t
    | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe env sigma sth,ic_unsafe env sigma ext)
    | Ring_mod(Pow_spec(t,spec)) -> set_once "power" power (t,spec)
    | Ring_mod(Sign_spec t) -> set_once "sign" sign t
    | Ring_mod(Div_spec t) -> set_once "div" div t
    | Inject i -> set_once "infinite property" inj (ic_unsafe env sigma i)) l;
  let k = match !kind with Some k -> k | None -> Abstract in
  (env, sigma, k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div)

let add_field_theory id t mods =
  let env = Global.env () in
  let sigma = Evd.from_env env in
  let (env,sigma,k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods env sigma mods in
  add_field_theory0 env sigma id t set k cst_tac inj (pre,post) power sign div

let ltac_field_structure e =
  let req = carg e.field_req in
  let cst_tac = tacarg e.field_cst_tac in
  let pow_tac = tacarg e.field_pow_tac in
  let field_ok = carg e.field_ok in
  let field_simpl_ok = carg e.field_simpl_ok in
  let field_simpl_eq_ok = carg e.field_simpl_eq_ok in
  let field_simpl_eq_in_ok = carg e.field_simpl_eq_in_ok in
  let cond_ok = carg e.field_cond in
  let pretac =  tacarg (CAst.make (TacFun ([Anonymous],e.field_pre_tac))) in
  let posttac = tacarg (CAst.make (TacFun ([Anonymous],e.field_post_tac))) in
  [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;
   field_simpl_eq_in_ok;cond_ok;pretac;posttac]

let field_lookup (f : Value.t) lH rl t =
  Proofview.Goal.enter begin fun gl ->
    let sigma = Tacmach.project gl in
    let env = Proofview.Goal.env gl in
    let rl = make_args_list sigma rl t in
    let e = find_field_structure env sigma rl in
    let sigma, c = make_term_list env sigma (EConstr.of_constr e.field_carrier) rl in
    let rl = Value.of_constr c in
    let sigma, l = make_hyp_list env sigma lH in
    let lH = Value.of_constr l in
    let field = ltac_field_structure e in
    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Value.apply f (field@[lH;rl]))
  end

quality93%

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.