summaryrefslogtreecommitdiff
path: root/plugins/subtac/subtac_command.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac/subtac_command.ml')
-rw-r--r--plugins/subtac/subtac_command.ml534
1 files changed, 534 insertions, 0 deletions
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
new file mode 100644
index 00000000..f2747225
--- /dev/null
+++ b/plugins/subtac/subtac_command.ml
@@ -0,0 +1,534 @@
+open Closure
+open RedFlags
+open Declarations
+open Entries
+open Libobject
+open Pattern
+open Matching
+open Pp
+open Rawterm
+open Sign
+open Tacred
+open Util
+open Names
+open Nameops
+open Libnames
+open Nametab
+open Pfedit
+open Proof_type
+open Refiner
+open Tacmach
+open Tactic_debug
+open Topconstr
+open Term
+open Termops
+open Tacexpr
+open Safe_typing
+open Typing
+open Hiddentac
+open Genarg
+open Decl_kinds
+open Mod_subst
+open Printer
+open Inductiveops
+open Syntax_def
+open Environ
+open Tactics
+open Tacticals
+open Tacinterp
+open Vernacexpr
+open Notation
+open Evd
+open Evarutil
+
+module SPretyping = Subtac_pretyping.Pretyping
+open Subtac_utils
+open Pretyping
+open Subtac_obligations
+
+(*********************************************************************)
+(* Functions to parse and interpret constructions *)
+
+let evar_nf isevars c =
+ Evarutil.nf_evar !isevars c
+
+let interp_gen kind isevars env
+ ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
+ c =
+ let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in
+ let c' = SPretyping.understand_tcc_evars isevars env kind c' in
+ evar_nf isevars c'
+
+let interp_constr isevars env c =
+ interp_gen (OfType None) isevars env c
+
+let interp_type_evars isevars env ?(impls=([],[])) c =
+ interp_gen IsType isevars env ~impls c
+
+let interp_casted_constr isevars env ?(impls=([],[])) c typ =
+ interp_gen (OfType (Some typ)) isevars env ~impls c
+
+let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ =
+ interp_gen (OfType (Some typ)) isevars env ~impls c
+
+let interp_open_constr isevars env c =
+ msgnl (str "Pretyping " ++ my_print_constr_expr c);
+ let c = Constrintern.intern_constr ( !isevars) env c in
+ let c' = SPretyping.understand_tcc_evars isevars env (OfType None) c in
+ evar_nf isevars c'
+
+let interp_constr_judgment isevars env c =
+ let j =
+ SPretyping.understand_judgment_tcc isevars env
+ (Constrintern.intern_constr ( !isevars) env c)
+ in
+ { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type }
+
+let locate_if_isevar loc na = function
+ | RHole _ ->
+ (try match na with
+ | Name id -> Reserve.find_reserved_type id
+ | Anonymous -> raise Not_found
+ with Not_found -> RHole (loc, Evd.BinderType na))
+ | x -> x
+
+let interp_binder sigma env na t =
+ let t = Constrintern.intern_gen true ( !sigma) env t in
+ SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_rawconstr t) na t)
+
+let interp_context_evars evdref env params =
+ let bl = Constrintern.intern_context false ( !evdref) env params in
+ let (env, par, _, impls) =
+ List.fold_left
+ (fun (env,params,n,impls) (na, k, b, t) ->
+ match b with
+ None ->
+ let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+ let t = SPretyping.understand_tcc_evars evdref env IsType t' in
+ let d = (na,None,t) in
+ let impls =
+ if k = Implicit then
+ let na = match na with Name n -> Some n | Anonymous -> None in
+ (ExplByPos (n, na), (true, true, true)) :: impls
+ else impls
+ in
+ (push_rel d env, d::params, succ n, impls)
+ | Some b ->
+ let c = SPretyping.understand_judgment_tcc evdref env b in
+ let d = (na, Some c.uj_val, c.uj_type) in
+ (push_rel d env,d::params, succ n, impls))
+ (env,[],1,[]) (List.rev bl)
+ in (env, par), impls
+
+(* try to find non recursive definitions *)
+
+let list_chop_hd i l = match list_chop i l with
+ | (l1,x::l2) -> (l1,x,l2)
+ | (x :: [], l2) -> ([], x, [])
+ | _ -> assert(false)
+
+let collect_non_rec env =
+ let rec searchrec lnonrec lnamerec ldefrec larrec nrec =
+ try
+ let i =
+ list_try_find_i
+ (fun i f ->
+ if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec
+ then i else failwith "try_find_i")
+ 0 lnamerec
+ in
+ let (lf1,f,lf2) = list_chop_hd i lnamerec in
+ let (ldef1,def,ldef2) = list_chop_hd i ldefrec in
+ let (lar1,ar,lar2) = list_chop_hd i larrec in
+ let newlnv =
+ try
+ match list_chop i nrec with
+ | (lnv1,_::lnv2) -> (lnv1@lnv2)
+ | _ -> [] (* nrec=[] for cofixpoints *)
+ with Failure "list_chop" -> []
+ in
+ searchrec ((f,def,ar)::lnonrec)
+ (lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv
+ with Failure "try_find_i" ->
+ (List.rev lnonrec,
+ (Array.of_list lnamerec, Array.of_list ldefrec,
+ Array.of_list larrec, Array.of_list nrec))
+ in
+ searchrec []
+
+let list_of_local_binders l =
+ let rec aux acc = function
+ Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl
+ | Topconstr.LocalRawAssum (nl, k, c) :: tl ->
+ aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl
+ | [] -> List.rev acc
+ in aux [] l
+
+let lift_binders k n l =
+ let rec aux n = function
+ | (id, t, c) :: tl -> (id, Option.map (liftn k n) t, liftn k n c) :: aux (pred n) tl
+ | [] -> []
+ in aux n l
+
+let rec gen_rels = function
+ 0 -> []
+ | n -> mkRel n :: gen_rels (pred n)
+
+let split_args n rel = match list_chop ((List.length rel) - n) rel with
+ (l1, x :: l2) -> l1, x, l2
+ | _ -> assert(false)
+
+open Coqlib
+
+let sigT = Lazy.lazy_from_fun build_sigma_type
+let sigT_info = lazy
+ { ci_ind = destInd (Lazy.force sigT).typ;
+ ci_npar = 2;
+ ci_cstr_nargs = [|2|];
+ ci_pp_info = { ind_nargs = 0; style = LetStyle }
+ }
+
+let telescope = function
+ | [] -> assert false
+ | [(n, None, t)] -> t, [n, Some (mkRel 1), t], mkRel 1
+ | (n, None, t) :: tl ->
+ let ty, tys, (k, constr) =
+ List.fold_left
+ (fun (ty, tys, (k, constr)) (n, b, t) ->
+ let pred = mkLambda (n, t, ty) in
+ let sigty = mkApp ((Lazy.force sigT).typ, [|t; pred|]) in
+ let intro = mkApp ((Lazy.force sigT).intro, [|lift k t; lift k pred; mkRel k; constr|]) in
+ (sigty, pred :: tys, (succ k, intro)))
+ (t, [], (2, mkRel 1)) tl
+ in
+ let (last, subst) = List.fold_right2
+ (fun pred (n, b, t) (prev, subst) ->
+ let proj1 = applistc (Lazy.force sigT).proj1 [t; pred; prev] in
+ let proj2 = applistc (Lazy.force sigT).proj2 [t; pred; prev] in
+ (lift 1 proj2, (n, Some proj1, t) :: subst))
+ (List.rev tys) tl (mkRel 1, [])
+ in ty, ((n, Some last, t) :: subst), constr
+
+ | _ -> raise (Invalid_argument "telescope")
+
+let nf_evar_context isevars ctx =
+ List.map (fun (n, b, t) ->
+ (n, Option.map (Evarutil.nf_evar isevars) b, Evarutil.nf_evar isevars t)) ctx
+
+let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
+ Coqlib.check_required_library ["Coq";"Program";"Wf"];
+ let sigma = Evd.empty in
+ let isevars = ref (Evd.create_evar_defs sigma) in
+ let env = Global.env() in
+ let _pr c = my_print_constr env c in
+ let _prr = Printer.pr_rel_context env in
+ let _prn = Printer.pr_named_context env in
+ let _pr_rel env = Printer.pr_rel_context env in
+ let (env', binders_rel), impls = interp_context_evars isevars env bl in
+ let len = List.length binders_rel in
+ let top_env = push_rel_context binders_rel env in
+ let top_arity = interp_type_evars isevars top_env arityc in
+ let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
+ let argtyp, letbinders, make = telescope binders_rel in
+ let argname = id_of_string "recarg" in
+ let arg = (Name argname, None, argtyp) in
+ let binders = letbinders @ [arg] in
+ let binders_env = push_rel_context binders_rel env in
+ let rel = interp_constr isevars env r in
+ let relty = type_of env !isevars rel in
+ let relargty =
+ let ctx, ar = Reductionops.splay_prod_n env !isevars 2 relty in
+ match ctx, kind_of_term ar with
+ | [(_, None, t); (_, None, u)], Sort (Prop Null)
+ when Reductionops.is_conv env !isevars t u -> t
+ | _, _ ->
+ user_err_loc (constr_loc r,
+ "Subtac_command.build_wellfounded",
+ my_print_constr env rel ++ str " is not an homogeneous binary relation.")
+ in
+ let measure = interp_casted_constr isevars binders_env measure relargty in
+ let wf_rel, wf_rel_fun, measure_fn =
+ let measure_body, measure =
+ it_mkLambda_or_LetIn measure letbinders,
+ it_mkLambda_or_LetIn measure binders
+ in
+ let comb = constr_of_global (Lazy.force measure_on_R_ref) in
+ let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
+ let wf_rel_fun x y =
+ mkApp (rel, [| subst1 x measure_body;
+ subst1 y measure_body |])
+ in wf_rel, wf_rel_fun, measure
+ in
+ let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |]) in
+ let argid' = id_of_string (string_of_id argname ^ "'") in
+ let wfarg len = (Name argid', None,
+ mkSubset (Name argid') argtyp
+ (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
+ in
+ let intern_bl = wfarg 1 :: [arg] in
+ let _intern_env = push_rel_context intern_bl env in
+ let proj = (Lazy.force sig_).Coqlib.proj1 in
+ let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
+ let projection = (* in wfarg :: arg :: before *)
+ mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
+ in
+ let top_arity_let = it_mkLambda_or_LetIn top_arity letbinders in
+ let intern_arity = substl [projection] top_arity_let in
+ (* substitute the projection of wfarg for something,
+ now intern_arity is in wfarg :: arg *)
+ let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
+ let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in
+ let curry_fun =
+ let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
+ let arg = mkApp ((Lazy.force sig_).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
+ let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
+ let rcurry = mkApp (rel, [| measure; lift len measure |]) in
+ let lam = (Name (id_of_string "recproof"), None, rcurry) in
+ let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in
+ let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in
+ (Name recname, Some body, ty)
+ in
+ let fun_bl = intern_fun_binder :: [arg] in
+ let lift_lets = Termops.lift_rel_context 1 letbinders in
+ let intern_body =
+ let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in
+ let (r, l, impls, scopes) =
+ Constrintern.compute_internalization_data env
+ Constrintern.Recursive full_arity impls
+ in
+ let newimpls = [(recname, (r, l, impls @
+ [Some (id_of_string "recproof", Impargs.Manual, (true, false))],
+ scopes @ [None]))] in
+ let newimpls = Constrintern.set_internalization_env_params newimpls [] in
+ interp_casted_constr isevars ~impls:newimpls
+ (push_rel_context ctx env) body (lift 1 top_arity)
+ in
+ let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
+ let prop = mkLambda (Name argname, argtyp, top_arity_let) in
+ let def =
+ mkApp (constr_of_global (Lazy.force fix_sub_ref),
+ [| argtyp ; wf_rel ;
+ make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
+ prop ; intern_body_lam |])
+ in
+ let _ = isevars := Evarutil.nf_evar_map !isevars in
+ let binders_rel = nf_evar_context !isevars binders_rel in
+ let binders = nf_evar_context !isevars binders in
+ let top_arity = Evarutil.nf_evar !isevars top_arity in
+ let hook, recname, typ =
+ if List.length binders_rel > 1 then
+ let name = add_suffix recname "_func" in
+ let hook l gr =
+ let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in
+ let ty = it_mkProd_or_LetIn top_arity binders_rel in
+ let ce =
+ { const_entry_body = Evarutil.nf_evar !isevars body;
+ const_entry_type = Some ty;
+ const_entry_opaque = false;
+ const_entry_boxed = false}
+ in
+ let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
+ let gr = ConstRef c in
+ if Impargs.is_implicit_args () || impls <> [] then
+ Impargs.declare_manual_implicits false gr impls
+ in
+ let typ = it_mkProd_or_LetIn top_arity binders in
+ hook, name, typ
+ else
+ let typ = it_mkProd_or_LetIn top_arity binders_rel in
+ let hook l gr =
+ if Impargs.is_implicit_args () || impls <> [] then
+ Impargs.declare_manual_implicits false gr impls
+ in hook, recname, typ
+ in
+ let fullcoqc = Evarutil.nf_evar !isevars def in
+ let fullctyp = Evarutil.nf_evar !isevars typ in
+ let evm = evars_of_term !isevars Evd.empty fullctyp in
+ let evm = evars_of_term !isevars evm fullcoqc in
+ let evm = non_instanciated_map env isevars evm in
+ let evars, _, evars_def, evars_typ =
+ Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp
+ in
+ Subtac_obligations.add_definition recname ~term:evars_def evars_typ evars ~hook
+
+let interp_fix_context evdref env fix =
+ interp_context_evars evdref env fix.Command.fix_binders
+
+let interp_fix_ccl evdref (env,_) fix =
+ interp_type_evars evdref env fix.Command.fix_type
+
+let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
+ let env = push_rel_context ctx env_rec in
+ let body = Option.map (fun c -> interp_casted_constr_evars evdref env ~impls c ccl) fix.Command.fix_body in
+ Option.map (fun c -> it_mkLambda_or_LetIn c ctx) body
+
+let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
+
+let prepare_recursive_declaration fixnames fixtypes fixdefs =
+ let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
+ let names = List.map (fun id -> Name id) fixnames in
+ (Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
+
+let rel_index n ctx =
+ list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx))
+
+let rec unfold f b =
+ match f b with
+ | Some (x, b') -> x :: unfold f b'
+ | None -> []
+
+let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
+ match n with
+ | Some (loc, n) -> [rel_index n fixctx]
+ | None ->
+ (* If recursive argument was not given by user, we try all args.
+ An earlier approach was to look only for inductive arguments,
+ but doing it properly involves delta-reduction, and it finally
+ doesn't seem to worth the effort (except for huge mutual
+ fixpoints ?) *)
+ let len = List.length fixctx in
+ unfold (function x when x = len -> None
+ | n -> Some (n, succ n)) 0
+
+let push_named_context = List.fold_right push_named
+
+let check_evars env initial_sigma evd c =
+ let sigma = evd in
+ let c = nf_evar sigma c in
+ let rec proc_rec c =
+ match kind_of_term c with
+ | Evar (evk,args) ->
+ assert (Evd.mem sigma evk);
+ if not (Evd.mem initial_sigma evk) then
+ let (loc,k) = evar_source evk evd in
+ (match k with
+ | QuestionMark _
+ | ImplicitArg (_, _, false) -> ()
+ | _ ->
+ let evi = nf_evar_info sigma (Evd.find sigma evk) in
+ Pretype_errors.error_unsolvable_implicit loc env sigma evi k None)
+ | _ -> iter_constr proc_rec c
+ in proc_rec c
+
+let out_def = function
+ | Some def -> def
+ | None -> error "Program Fixpoint needs defined bodies."
+
+let interp_recursive fixkind l boxed =
+ let env = Global.env() in
+ let fixl, ntnl = List.split l in
+ let kind = fixkind <> IsCoFixpoint in
+ let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in
+
+ (* Interp arities allowing for unresolved types *)
+ let evdref = ref Evd.empty in
+ let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in
+ let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
+ let fixtypes = List.map2 build_fix_type fixctxs fixccls in
+ let rec_sign =
+ List.fold_left2 (fun env' id t ->
+ let sort = Retyping.get_type_of env !evdref t in
+ let fixprot =
+ try mkApp (Lazy.force Subtac_utils.fix_proto, [|sort; t|])
+ with e -> t
+ in
+ (id,None,fixprot) :: env')
+ [] fixnames fixtypes
+ in
+ let env_rec = push_named_context rec_sign env in
+
+ (* Get interpretation metadatas *)
+ let impls = Constrintern.compute_full_internalization_env env
+ Constrintern.Recursive [] fixnames fixtypes fiximps
+ in
+ let notations = List.flatten ntnl in
+
+ (* Interp bodies with rollback because temp use of notations/implicit *)
+ let fixdefs =
+ States.with_state_protection (fun () ->
+ List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
+ list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
+ () in
+
+ let fixdefs = List.map out_def fixdefs in
+
+ (* Instantiate evars and check all are resolved *)
+ let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in
+ let evd = Typeclasses.resolve_typeclasses
+ ~onlyargs:true ~split:true ~fail:false env_rec evd
+ in
+ let evd = Evarutil.nf_evar_map evd in
+ let fixdefs = List.map (nf_evar evd) fixdefs in
+ let fixtypes = List.map (nf_evar evd) fixtypes in
+ let rec_sign = nf_named_context_evar evd rec_sign in
+
+ let recdefs = List.length rec_sign in
+ List.iter (check_evars env_rec Evd.empty evd) fixdefs;
+ List.iter (check_evars env Evd.empty evd) fixtypes;
+ Command.check_mutuality env kind (List.combine fixnames fixdefs);
+
+ (* Russell-specific code *)
+
+ (* Get the interesting evars, those that were not instanciated *)
+ let isevars = Evd.undefined_evars evd in
+ let evm = isevars in
+ (* Solve remaining evars *)
+ let rec collect_evars id def typ imps =
+ (* Generalize by the recursive prototypes *)
+ let def =
+ Termops.it_mkNamedLambda_or_LetIn def rec_sign
+ and typ =
+ Termops.it_mkNamedProd_or_LetIn typ rec_sign
+ in
+ let evm' = Subtac_utils.evars_of_term evm Evd.empty def in
+ let evm' = Subtac_utils.evars_of_term evm evm' typ in
+ let evars, _, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in
+ (id, def, typ, imps, evars)
+ in
+ let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in
+ (match fixkind with
+ | IsFixpoint wfl ->
+ let possible_indexes =
+ list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
+ let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
+ Array.of_list fixtypes,
+ Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
+ in
+ let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
+ list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) l
+ | IsCoFixpoint -> ());
+ Subtac_obligations.add_mutual_definitions defs notations fixkind
+
+let out_n = function
+ Some n -> n
+ | None -> raise Not_found
+
+let build_recursive l b =
+ let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
+ match g, l with
+ [(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
+ ignore(build_wellfounded (id, n, bl, typ, out_def def) r
+ (match n with Some n -> mkIdentC (snd n) | None ->
+ errorlabstrm "Subtac_command.build_recursive"
+ (str "Recursive argument required for well-founded fixpoints"))
+ ntn false)
+
+ | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] ->
+ ignore(build_wellfounded (id, n, bl, typ, out_def def) (Option.default (CRef lt_ref) r)
+ m ntn false)
+
+ | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
+ let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) ->
+ ({Command.fix_name = id; Command.fix_binders = bl;
+ Command.fix_body = def; Command.fix_type = typ},ntn)) l
+ in interp_recursive (IsFixpoint g) fixl b
+ | _, _ ->
+ errorlabstrm "Subtac_command.build_recursive"
+ (str "Well-founded fixpoints not allowed in mutually recursive blocks")
+
+let build_corecursive l b =
+ let fixl = List.map (fun (((_,id),bl,typ,def),ntn) ->
+ ({Command.fix_name = id; Command.fix_binders = bl;
+ Command.fix_body = def; Command.fix_type = typ},ntn))
+ l in
+ interp_recursive IsCoFixpoint fixl b
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-02 10:17:39 +0000