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.ml544
1 files changed, 0 insertions, 544 deletions
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
deleted file mode 100644
index 537a8301..00000000
--- a/plugins/subtac/subtac_command.ml
+++ /dev/null
@@ -1,544 +0,0 @@
-open Closure
-open RedFlags
-open Declarations
-open Entries
-open Libobject
-open Pattern
-open Matching
-open Pp
-open Glob_term
-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 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=Constrintern.empty_internalization_env) ?(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=Constrintern.empty_internalization_env) c =
- interp_gen IsType isevars env ~impls c
-
-let interp_casted_constr isevars env ?(impls=Constrintern.empty_internalization_env) c typ =
- interp_gen (OfType (Some typ)) isevars env ~impls c
-
-let interp_casted_constr_evars isevars env ?(impls=Constrintern.empty_internalization_env) 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
- | GHole _ ->
- (try match na with
- | Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id)
- | Anonymous -> raise Not_found
- with Not_found -> GHole (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_glob_constr t) na t)
-
-let interp_context_evars evdref env params =
- let int_env, bl = Constrintern.intern_context false !evdref env Constrintern.empty_internalization_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_glob_constr 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 (Termops.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_ndecls = [|2|];
- ci_pp_info = { ind_nargs = 0; style = LetStyle }
- }
-
-let rec 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
-
- | (n, Some b, t) :: tl -> let ty, subst, term = telescope tl in
- ty, ((n, Some b, t) :: subst), lift 1 term
-
-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 =
- 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 error () =
- user_err_loc (constr_loc r,
- "Subtac_command.build_wellfounded",
- my_print_constr env rel ++ str " is not an homogeneous binary relation.")
- in
- try
- 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
- | _, _ -> error ()
- with e when Errors.noncritical e -> error ()
- 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 (delayed_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 (delayed_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 = (delayed_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 ((delayed_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 = Idmap.singleton recname
- (r, l, impls @ [(Some (id_of_string "recproof", Impargs.Manual, (true, false)))],
- scopes @ [None]) 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 (delayed_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_secctx = None;
- const_entry_type = Some ty;
- const_entry_opaque = 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 find_annot loc id ctx =
- try rel_index id ctx
- with Not_found ->
- user_err_loc(loc,"",
- str "No parameter named " ++ Nameops.pr_id id ++ str".")
-
-let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
- match n with
- | Some (loc, id) -> [find_annot loc id 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 =
- 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 (delayed_force Subtac_utils.fix_proto, [|sort; t|])
- with e when Errors.noncritical 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_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
- ~filter:Typeclasses.no_goals ~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 =
- 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)
-
- | [(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)
-
- | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
- let fixl = List.map (fun (((_,id),(n,ro),bl,typ,def),ntn) ->
- ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = n;
- Command.fix_body = def; Command.fix_type = typ},ntn)) l
- in interp_recursive (IsFixpoint g) fixl
- | _, _ ->
- errorlabstrm "Subtac_command.build_recursive"
- (str "Well-founded fixpoints not allowed in mutually recursive blocks")
-
-let build_corecursive l =
- let fixl = List.map (fun (((_,id),bl,typ,def),ntn) ->
- ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = None;
- Command.fix_body = def; Command.fix_type = typ},ntn))
- l in
- interp_recursive IsCoFixpoint fixl
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-01 03:15:58 +0000