diff options
Diffstat (limited to 'plugins/subtac')
33 files changed, 0 insertions, 6752 deletions
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml deleted file mode 100644 index f4d8b769..00000000 --- a/plugins/subtac/eterm.ml +++ /dev/null @@ -1,259 +0,0 @@ -(** - - Get types of existentials ; - - Flatten dependency tree (prefix order) ; - - Replace existentials by De Bruijn indices in term, applied to the right arguments ; - - Apply term prefixed by quantification on "existentials". -*) - -open Term -open Sign -open Names -open Evd -open List -open Pp -open Util -open Subtac_utils -open Proof_type - -let trace s = - if !Flags.debug then (msgnl s; msgerr s) - else () - -let succfix (depth, fixrels) = - (succ depth, List.map succ fixrels) - -type oblinfo = - { ev_name: int * identifier; - ev_hyps: named_context; - ev_status: obligation_definition_status; - ev_chop: int option; - ev_src: hole_kind located; - ev_typ: types; - ev_tac: tactic option; - ev_deps: Intset.t } - -(* spiwack: Store field for internalizing ev_tac in evar_infos' evar_extra. *) -open Store.Field -let evar_tactic = Store.field () - -(** Substitute evar references in t using De Bruijn indices, - where n binders were passed through. *) - -let subst_evar_constr evs n idf t = - let seen = ref Intset.empty in - let transparent = ref Idset.empty in - let evar_info id = List.assoc id evs in - let rec substrec (depth, fixrels) c = match kind_of_term c with - | Evar (k, args) -> - let { ev_name = (id, idstr) ; - ev_hyps = hyps ; ev_chop = chop } = - try evar_info k - with Not_found -> - anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found") - in - seen := Intset.add id !seen; - (* Evar arguments are created in inverse order, - and we must not apply to defined ones (i.e. LetIn's) - *) - let args = - let n = match chop with None -> 0 | Some c -> c in - let (l, r) = list_chop n (List.rev (Array.to_list args)) in - List.rev r - in - let args = - let rec aux hyps args acc = - match hyps, args with - ((_, None, _) :: tlh), (c :: tla) -> - aux tlh tla ((substrec (depth, fixrels) c) :: acc) - | ((_, Some _, _) :: tlh), (_ :: tla) -> - aux tlh tla acc - | [], [] -> acc - | _, _ -> acc (*failwith "subst_evars: invalid argument"*) - in aux hyps args [] - in - if List.exists (fun x -> match kind_of_term x with Rel n -> List.mem n fixrels | _ -> false) args then - transparent := Idset.add idstr !transparent; - mkApp (idf idstr, Array.of_list args) - | Fix _ -> - map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c - | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c - in - let t' = substrec (0, []) t in - t', !seen, !transparent - - -(** Substitute variable references in t using De Bruijn indices, - where n binders were passed through. *) -let subst_vars acc n t = - let var_index id = Util.list_index id acc in - let rec substrec depth c = match kind_of_term c with - | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c) - | _ -> map_constr_with_binders succ substrec depth c - in - substrec 0 t - -(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ]) - to a product : forall H1 : t1, ..., forall Hn : tn, concl. - Changes evars and hypothesis references to variable references. -*) -let etype_of_evar evs hyps concl = - let rec aux acc n = function - (id, copt, t) :: tl -> - let t', s, trans = subst_evar_constr evs n mkVar t in - let t'' = subst_vars acc 0 t' in - let rest, s', trans' = aux (id :: acc) (succ n) tl in - let s' = Intset.union s s' in - let trans' = Idset.union trans trans' in - (match copt with - Some c -> - let c', s'', trans'' = subst_evar_constr evs n mkVar c in - let c' = subst_vars acc 0 c' in - mkNamedProd_or_LetIn (id, Some c', t'') rest, - Intset.union s'' s', - Idset.union trans'' trans' - | None -> - mkNamedProd_or_LetIn (id, None, t'') rest, s', trans') - | [] -> - let t', s, trans = subst_evar_constr evs n mkVar concl in - subst_vars acc 0 t', s, trans - in aux [] 0 (rev hyps) - - -open Tacticals - -let trunc_named_context n ctx = - let len = List.length ctx in - list_firstn (len - n) ctx - -let rec chop_product n t = - if n = 0 then Some t - else - match kind_of_term t with - | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None - | _ -> None - -let evars_of_evar_info evi = - Intset.union (Evarutil.evars_of_term evi.evar_concl) - (Intset.union - (match evi.evar_body with - | Evar_empty -> Intset.empty - | Evar_defined b -> Evarutil.evars_of_term b) - (Evarutil.evars_of_named_context (evar_filtered_context evi))) - -let evar_dependencies evm oev = - let one_step deps = - Intset.fold (fun ev s -> - let evi = Evd.find evm ev in - let deps' = evars_of_evar_info evi in - if Intset.mem oev deps' then - raise (Invalid_argument ("Ill-formed evar map: cycle detected for evar " ^ string_of_int oev)) - else Intset.union deps' s) - deps deps - in - let rec aux deps = - let deps' = one_step deps in - if Intset.equal deps deps' then deps - else aux deps' - in aux (Intset.singleton oev) - -let move_after (id, ev, deps as obl) l = - let rec aux restdeps = function - | (id', _, _) as obl' :: tl -> - let restdeps' = Intset.remove id' restdeps in - if Intset.is_empty restdeps' then - obl' :: obl :: tl - else obl' :: aux restdeps' tl - | [] -> [obl] - in aux (Intset.remove id deps) l - -let sort_dependencies evl = - let rec aux l found list = - match l with - | (id, ev, deps) as obl :: tl -> - let found' = Intset.union found (Intset.singleton id) in - if Intset.subset deps found' then - aux tl found' (obl :: list) - else aux (move_after obl tl) found list - | [] -> List.rev list - in aux evl Intset.empty [] - -let map_evar_body f = function - | Evar_empty -> Evar_empty - | Evar_defined c -> Evar_defined (f c) - -open Environ - -let map_evar_info f evi = - { evi with evar_hyps = val_of_named_context (map_named_context f (named_context_of_val evi.evar_hyps)); - evar_concl = f evi.evar_concl; - evar_body = map_evar_body f evi.evar_body } - -let eterm_obligations env name isevars evm fs ?status t ty = - (* 'Serialize' the evars *) - let nc = Environ.named_context env in - let nc_len = Sign.named_context_length nc in - let evl = List.rev (to_list evm) in - let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in - let sevl = sort_dependencies evl in - let evl = List.map (fun (id, ev, _) -> id, ev) sevl in - let evn = - let i = ref (-1) in - List.rev_map (fun (id, ev) -> incr i; - (id, (!i, id_of_string - (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), - ev)) evl - in - let evts = - (* Remove existential variables in types and build the corresponding products *) - fold_right - (fun (id, (n, nstr), ev) l -> - let hyps = Evd.evar_filtered_context ev in - let hyps = trunc_named_context nc_len hyps in - let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in - let evtyp, hyps, chop = - match chop_product fs evtyp with - | Some t -> t, trunc_named_context fs hyps, fs - | None -> evtyp, hyps, 0 - in - let loc, k = evar_source id isevars in - let status = match k with QuestionMark o -> Some o | _ -> status in - let status, chop = match status with - | Some (Define true as stat) -> - if chop <> fs then Define false, None - else stat, Some chop - | Some s -> s, None - | None -> Define true, None - in - let tac = match evar_tactic.get ev.evar_extra with - | Some t -> - if Dyn.tag t = "tactic" then - Some (Tacinterp.interp - (Tacinterp.globTacticIn (Tacinterp.tactic_out t))) - else None - | None -> None - in - let info = { ev_name = (n, nstr); - ev_hyps = hyps; ev_status = status; ev_chop = chop; - ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac } - in (id, info) :: l) - evn [] - in - let t', _, transparent = (* Substitute evar refs in the term by variables *) - subst_evar_constr evts 0 mkVar t - in - let ty, _, _ = subst_evar_constr evts 0 mkVar ty in - let evars = - List.map (fun (ev, info) -> - let { ev_name = (_, name); ev_status = status; - ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info - in - let status = match status with - | Define true when Idset.mem name transparent -> Define false - | _ -> status - in name, typ, src, status, deps, tac) evts - in - let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in - let evmap f c = pi1 (subst_evar_constr evts 0 f c) in - Array.of_list (List.rev evars), (evnames, evmap), t', ty - -let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli deleted file mode 100644 index 35744b71..00000000 --- a/plugins/subtac/eterm.mli +++ /dev/null @@ -1,33 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Environ -open Tacmach -open Term -open Evd -open Names -open Util -open Tacinterp - -val mkMetas : int -> constr list - -val evar_dependencies : evar_map -> int -> Intset.t -val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * Intset.t) list - -(* env, id, evars, number of function prototypes to try to clear from - evars contexts, object and type *) -val eterm_obligations : env -> identifier -> evar_map -> evar_map -> int -> - ?status:obligation_definition_status -> constr -> types -> - (identifier * types * hole_kind located * obligation_definition_status * Intset.t * - tactic option) array - (* Existential key, obl. name, type as product, location of the original evar, associated tactic, - status and dependencies as indexes into the array *) - * ((existential_key * identifier) list * ((identifier -> constr) -> constr -> constr)) * constr * types - (* Translations from existential identifiers to obligation identifiers - and for terms with existentials to closed terms, given a - translation from obligation identifiers to constrs, new term, new type *) diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4 deleted file mode 100644 index c89d135f..00000000 --- a/plugins/subtac/g_subtac.ml4 +++ /dev/null @@ -1,167 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i camlp4deps: "parsing/grammar.cma" i*) - -(* - Syntax for the subtac terms and types. - Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *) - - -open Flags -open Util -open Names -open Nameops -open Vernacentries -open Reduction -open Term -open Libnames -open Topconstr - -(* We define new entries for programs, with the use of this module - * Subtac. These entries are named Subtac.<foo> - *) - -module Gram = Pcoq.Gram -module Vernac = Pcoq.Vernac_ -module Tactic = Pcoq.Tactic - -module SubtacGram = -struct - let gec s = Gram.entry_create ("Subtac."^s) - (* types *) - let subtac_gallina_loc : Vernacexpr.vernac_expr located Gram.entry = gec "subtac_gallina_loc" - - let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "subtac_withtac" -end - -open Glob_term -open SubtacGram -open Util -open Pcoq -open Prim -open Constr -let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig")) - -GEXTEND Gram - GLOBAL: subtac_gallina_loc typeclass_constraint subtac_withtac; - - subtac_gallina_loc: - [ [ g = Vernac.gallina -> loc, g - | g = Vernac.gallina_ext -> loc, g ] ] - ; - - subtac_withtac: - [ [ "with"; t = Tactic.tactic -> Some t - | -> None ] ] - ; - - Constr.closed_binder: - [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> - let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in - [LocalRawAssum ([id], default_binder_kind, typ)] - ] ]; - - END - - -type 'a gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a) Genarg.abstract_argument_type - -let (wit_subtac_gallina_loc : Genarg.tlevel gallina_loc_argtype), - (globwit_subtac_gallina_loc : Genarg.glevel gallina_loc_argtype), - (rawwit_subtac_gallina_loc : Genarg.rlevel gallina_loc_argtype) = - Genarg.create_arg None "subtac_gallina_loc" - -type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type - -let (wit_subtac_withtac : Genarg.tlevel withtac_argtype), - (globwit_subtac_withtac : Genarg.glevel withtac_argtype), - (rawwit_subtac_withtac : Genarg.rlevel withtac_argtype) = - Genarg.create_arg None "subtac_withtac" - -VERNAC COMMAND EXTEND Subtac -[ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ] - END - -let try_catch_exn f e = - try f e - with exn when Errors.noncritical exn -> - errorlabstrm "Program" (Errors.print exn) - -let subtac_obligation e = try_catch_exn Subtac_obligations.subtac_obligation e -let next_obligation e = try_catch_exn Subtac_obligations.next_obligation e -let try_solve_obligation e = try_catch_exn Subtac_obligations.try_solve_obligation e -let try_solve_obligations e = try_catch_exn Subtac_obligations.try_solve_obligations e -let solve_all_obligations e = try_catch_exn Subtac_obligations.solve_all_obligations e -let admit_obligations e = try_catch_exn Subtac_obligations.admit_obligations e - -VERNAC COMMAND EXTEND Subtac_Obligations -| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) subtac_withtac(tac) ] -> - [ subtac_obligation (num, Some name, Some t) tac ] -| [ "Obligation" integer(num) "of" ident(name) subtac_withtac(tac) ] -> - [ subtac_obligation (num, Some name, None) tac ] -| [ "Obligation" integer(num) ":" lconstr(t) subtac_withtac(tac) ] -> - [ subtac_obligation (num, None, Some t) tac ] -| [ "Obligation" integer(num) subtac_withtac(tac) ] -> - [ subtac_obligation (num, None, None) tac ] -| [ "Next" "Obligation" "of" ident(name) subtac_withtac(tac) ] -> - [ next_obligation (Some name) tac ] -| [ "Next" "Obligation" subtac_withtac(tac) ] -> [ next_obligation None tac ] -END - -VERNAC COMMAND EXTEND Subtac_Solve_Obligation -| [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] -> - [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligation" integer(num) "using" tactic(t) ] -> - [ try_solve_obligation num None (Some (Tacinterp.interp t)) ] - END - -VERNAC COMMAND EXTEND Subtac_Solve_Obligations -| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> - [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" "using" tactic(t) ] -> - [ try_solve_obligations None (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" ] -> - [ try_solve_obligations None None ] - END - -VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations -| [ "Solve" "All" "Obligations" "using" tactic(t) ] -> - [ solve_all_obligations (Some (Tacinterp.interp t)) ] -| [ "Solve" "All" "Obligations" ] -> - [ solve_all_obligations None ] - END - -VERNAC COMMAND EXTEND Subtac_Admit_Obligations -| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ] -| [ "Admit" "Obligations" ] -> [ admit_obligations None ] - END - -VERNAC COMMAND EXTEND Subtac_Set_Solver -| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ - Subtac_obligations.set_default_tactic - (Vernacexpr.use_section_locality ()) - (Tacinterp.glob_tactic t) ] -END - -open Pp - -VERNAC COMMAND EXTEND Subtac_Show_Solver -| [ "Show" "Obligation" "Tactic" ] -> [ - msgnl (str"Program obligation tactic is " ++ Subtac_obligations.print_default_tactic ()) ] -END - -VERNAC COMMAND EXTEND Subtac_Show_Obligations -| [ "Obligations" "of" ident(name) ] -> [ Subtac_obligations.show_obligations (Some name) ] -| [ "Obligations" ] -> [ Subtac_obligations.show_obligations None ] -END - -VERNAC COMMAND EXTEND Subtac_Show_Preterm -| [ "Preterm" "of" ident(name) ] -> [ Subtac_obligations.show_term (Some name) ] -| [ "Preterm" ] -> [ Subtac_obligations.show_term None ] -END diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml deleted file mode 100644 index 89d9050c..00000000 --- a/plugins/subtac/subtac.ml +++ /dev/null @@ -1,226 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Compat -open Global -open Pp -open Util -open Names -open Sign -open Evd -open Term -open Termops -open Namegen -open Reductionops -open Environ -open Type_errors -open Typeops -open Libnames -open Classops -open List -open Recordops -open Evarutil -open Pretype_errors -open Glob_term -open Evarconv -open Pattern -open Vernacexpr - -open Subtac_coercion -open Subtac_utils -open Coqlib -open Printer -open Subtac_errors -open Eterm - -let require_library dirpath = - let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in - Library.require_library [qualid] None - -open Pp -open Ppconstr -open Decl_kinds -open Tacinterp -open Tacexpr - -let solve_tccs_in_type env id isevars evm c typ = - if not (Evd.is_empty evm) then - let stmt_id = Nameops.add_suffix id "_stmt" in - let obls, _, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in - match Subtac_obligations.add_definition stmt_id ~term:c' typ obls with - | Subtac_obligations.Defined cst -> constant_value (Global.env()) - (match cst with ConstRef kn -> kn | _ -> assert false) - | _ -> - errorlabstrm "start_proof" - (str "The statement obligations could not be resolved automatically, " ++ spc () ++ - str "write a statement definition first.") - else - let _ = Typeops.infer_type env c in c - - -let start_proof_com env isevars sopt kind (bl,t) hook = - let id = match sopt with - | Some (loc,id) -> - (* We check existence here: it's a bit late at Qed time *) - if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then - user_err_loc (loc,"start_proof",pr_id id ++ str " already exists"); - id - | None -> - next_global_ident_away (id_of_string "Unnamed_thm") - (Pfedit.get_all_proof_names ()) - in - let evm, c, typ, imps = - Subtac_pretyping.subtac_process ~is_type:true env isevars id [] (Topconstr.prod_constr_expr t bl) None - in - let c = solve_tccs_in_type env id isevars evm c typ in - Lemmas.start_proof id kind c (fun loc gr -> - Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true [imps]; - hook loc gr) - -let start_proof_and_print env isevars idopt k t hook = - start_proof_com env isevars idopt k t hook; - Vernacentries.print_subgoals () - -let _ = Detyping.set_detype_anonymous (fun loc n -> GVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n))) - -let assumption_message id = - Flags.if_verbose message ((string_of_id id) ^ " is assumed") - -let declare_assumptions env isevars idl is_coe k bl c nl = - if not (Pfedit.refining ()) then - let id = snd (List.hd idl) in - let evm, c, typ, imps = - Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr c bl) None - in - let c = solve_tccs_in_type env id isevars evm c typ in - List.iter (Command.declare_assumption is_coe k c imps false nl) idl - else - errorlabstrm "Command.Assumption" - (str "Cannot declare an assumption while in proof editing mode.") - -let dump_constraint ty ((loc, n), _, _) = - match n with - | Name id -> Dumpglob.dump_definition (loc, id) false ty - | Anonymous -> () - -let dump_variable lid = () - -let vernac_assumption env isevars kind l nl = - let global = fst kind = Global in - List.iter (fun (is_coe,(idl,c)) -> - if Dumpglob.dump () then - List.iter (fun lid -> - if global then Dumpglob.dump_definition lid (not global) "ax" - else dump_variable lid) idl; - declare_assumptions env isevars idl is_coe kind [] c nl) l - -let check_fresh (loc,id) = - if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then - user_err_loc (loc,"",pr_id id ++ str " already exists") - -let subtac (loc, command) = - check_required_library ["Coq";"Init";"Datatypes"]; - check_required_library ["Coq";"Init";"Specif"]; - let env = Global.env () in - let isevars = ref (create_evar_defs Evd.empty) in - try - match command with - | VernacDefinition (defkind, (_, id as lid), expr, hook) -> - check_fresh lid; - Dumpglob.dump_definition lid false "def"; - (match expr with - | ProveBody (bl, t) -> - start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) - (fun _ _ -> ()) - | DefineBody (bl, _, c, tycon) -> - ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon)) - | VernacFixpoint l -> - List.iter (fun ((lid, _, _, _, _), _) -> - check_fresh lid; - Dumpglob.dump_definition lid false "fix") l; - let _ = trace (str "Building fixpoint") in - ignore(Subtac_command.build_recursive l) - - | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) -> - if guard <> None then - error "Do not support building theorems as a fixpoint."; - Dumpglob.dump_definition id false "prf"; - if not(Pfedit.refining ()) then - if lettop then - errorlabstrm "Subtac_command.StartProof" - (str "Let declarations can only be used in proof editing mode"); - if Lib.is_modtype () then - errorlabstrm "Subtac_command.StartProof" - (str "Proof editing mode not supported in module types"); - check_fresh id; - start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook - - | VernacAssumption (stre,nl,l) -> - vernac_assumption env isevars stre l nl - - | VernacInstance (abst, glob, sup, is, props, pri) -> - dump_constraint "inst" is; - if abst then - error "Declare Instance not supported here."; - ignore(Subtac_classes.new_instance ~global:glob sup is props pri) - - | VernacCoFixpoint l -> - if Dumpglob.dump () then - List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l; - ignore(Subtac_command.build_corecursive l) - - (*| VernacEndProof e -> - subtac_end_proof e*) - - | _ -> user_err_loc (loc,"", str ("Invalid Program command")) - with - | Typing_error e -> - msg_warning (str "Type error in Program tactic:"); - let cmds = - (match e with - | NonFunctionalApp (loc, x, mux, e) -> - str "non functional application of term " ++ - e ++ str " to function " ++ x ++ str " of (mu) type " ++ mux - | NonSigma (loc, t) -> - str "Term is not of Sigma type: " ++ t - | NonConvertible (loc, x, y) -> - str "Unconvertible terms:" ++ spc () ++ - x ++ spc () ++ str "and" ++ spc () ++ y - | IllSorted (loc, t) -> - str "Term is ill-sorted:" ++ spc () ++ t - ) - in msg_warning cmds - - | Subtyping_error e -> - msg_warning (str "(Program tactic) Subtyping error:"); - let cmds = - match e with - | UncoercibleInferType (loc, x, y) -> - str "Uncoercible terms:" ++ spc () - ++ x ++ spc () ++ str "and" ++ spc () ++ y - | UncoercibleInferTerm (loc, x, y, tx, ty) -> - str "Uncoercible terms:" ++ spc () - ++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x - ++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y - | UncoercibleRewrite (x, y) -> - str "Uncoercible terms:" ++ spc () - ++ x ++ spc () ++ str "and" ++ spc () ++ y - in msg_warning cmds - - | Cases.PatternMatchingError (env, exn) as e -> raise e - - | Type_errors.TypeError (env, exn) as e -> raise e - - | Pretype_errors.PretypeError (env, _, exn) as e -> raise e - - | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) | - Loc.Exc_located (loc, e') as e) -> raise e - - | reraise -> - (* msg_warning (str "Uncaught exception: " ++ Errors.print e); *) - raise reraise diff --git a/plugins/subtac/subtac.mli b/plugins/subtac/subtac.mli deleted file mode 100644 index b51150aa..00000000 --- a/plugins/subtac/subtac.mli +++ /dev/null @@ -1,2 +0,0 @@ -val require_library : string -> unit -val subtac : Util.loc * Vernacexpr.vernac_expr -> unit diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml deleted file mode 100644 index 9ff8ba50..00000000 --- a/plugins/subtac/subtac_cases.ml +++ /dev/null @@ -1,2023 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Cases -open Util -open Names -open Nameops -open Term -open Termops -open Namegen -open Declarations -open Inductiveops -open Environ -open Sign -open Reductionops -open Typeops -open Type_errors -open Glob_term -open Retyping -open Pretype_errors -open Evarutil -open Evarconv -open Subtac_utils - -(************************************************************************) -(* Pattern-matching compilation (Cases) *) -(************************************************************************) - -(************************************************************************) -(* Configuration, errors and warnings *) - -open Pp - -let mssg_may_need_inversion () = - str "Found a matching with no clauses on a term unknown to have an empty inductive type" - -(* Utils *) -let make_anonymous_patvars = - list_tabulate (fun _ -> PatVar (dummy_loc,Anonymous)) - -(* Environment management *) -let push_rels vars env = List.fold_right push_rel vars env - -(* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize - over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *) - -let regeneralize_rel i k j = if j = i+k then k else if j < i+k then j else j - -let rec regeneralize_index i k t = match kind_of_term t with - | Rel j when j = i+k -> mkRel (k+1) - | Rel j when j < i+k -> t - | Rel j when j > i+k -> t - | _ -> map_constr_with_binders succ (regeneralize_index i) k t - -type alias_constr = - | DepAlias - | NonDepAlias - -let mkSpecialLetInJudge j (na,(deppat,nondeppat,d,t)) = - { uj_val = - (match d with - | DepAlias -> mkLetIn (na,deppat,t,j.uj_val) - | NonDepAlias -> - if (not (dependent (mkRel 1) j.uj_type)) - or (* A leaf: *) isRel deppat - then - (* The body of pat is not needed to type j - see *) - (* insert_aliases - and both deppat and nondeppat have the *) - (* same type, then one can freely substitute one by the other *) - subst1 nondeppat j.uj_val - else - (* The body of pat is not needed to type j but its value *) - (* is dependent in the type of j; our choice is to *) - (* enforce this dependency *) - mkLetIn (na,deppat,t,j.uj_val)); - uj_type = subst1 deppat j.uj_type } - -(**********************************************************************) -(* Structures used in compiling pattern-matching *) - -type rhs = - { rhs_env : env; - avoid_ids : identifier list; - it : glob_constr; - } - -type equation = - { patterns : cases_pattern list; - rhs : rhs; - alias_stack : name list; - eqn_loc : loc; - used : bool ref } - -type matrix = equation list - -(* 1st argument of IsInd is the original ind before extracting the summary *) -type tomatch_type = - | IsInd of types * inductive_type - | NotInd of constr option * types - -type tomatch_status = - | Pushed of ((constr * tomatch_type) * int list) - | Alias of (constr * constr * alias_constr * constr) - | Abstract of rel_declaration - -type tomatch_stack = tomatch_status list - -(* The type [predicate_signature] types the terms to match and the rhs: - - - [PrLetIn (names,dep,pred)] types a pushed term ([Pushed]), - if dep<>Anonymous, the term is dependent, let n=|names|, if - n<>0 then the type of the pushed term is necessarily an - inductive with n real arguments. Otherwise, it may be - non inductive, or inductive without real arguments, or inductive - originating from a subterm in which case real args are not dependent; - it accounts for n+1 binders if dep or n binders if not dep - - [PrProd] types abstracted term ([Abstract]); it accounts for one binder - - [PrCcl] types the right-hand side - - Aliases [Alias] have no trace in [predicate_signature] -*) - -type predicate_signature = - | PrLetIn of (name list * name) * predicate_signature - | PrProd of predicate_signature - | PrCcl of constr - -(* We keep a constr for aliases and a cases_pattern for error message *) - -type alias_builder = - | AliasLeaf - | AliasConstructor of constructor - -type pattern_history = - | Top - | MakeAlias of alias_builder * pattern_continuation - -and pattern_continuation = - | Continuation of int * cases_pattern list * pattern_history - | Result of cases_pattern list - -let start_history n = Continuation (n, [], Top) - -let feed_history arg = function - | Continuation (n, l, h) when n>=1 -> - Continuation (n-1, arg :: l, h) - | Continuation (n, _, _) -> - anomaly ("Bad number of expected remaining patterns: "^(string_of_int n)) - | Result _ -> - anomaly "Exhausted pattern history" - -(* This is for non exhaustive error message *) - -let rec glob_pattern_of_partial_history args2 = function - | Continuation (n, args1, h) -> - let args3 = make_anonymous_patvars (n - (List.length args2)) in - build_glob_pattern (List.rev_append args1 (args2@args3)) h - | Result pl -> pl - -and build_glob_pattern args = function - | Top -> args - | MakeAlias (AliasLeaf, rh) -> - assert (args = []); - glob_pattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh - | MakeAlias (AliasConstructor pci, rh) -> - glob_pattern_of_partial_history - [PatCstr (dummy_loc, pci, args, Anonymous)] rh - -let complete_history = glob_pattern_of_partial_history [] - -(* This is to build glued pattern-matching history and alias bodies *) - -let rec simplify_history = function - | Continuation (0, l, Top) -> Result (List.rev l) - | Continuation (0, l, MakeAlias (f, rh)) -> - let pargs = List.rev l in - let pat = match f with - | AliasConstructor pci -> - PatCstr (dummy_loc,pci,pargs,Anonymous) - | AliasLeaf -> - assert (l = []); - PatVar (dummy_loc, Anonymous) in - feed_history pat rh - | h -> h - -(* Builds a continuation expecting [n] arguments and building [ci] applied - to this [n] arguments *) - -let push_history_pattern n current cont = - Continuation (n, [], MakeAlias (current, cont)) - -(* A pattern-matching problem has the following form: - - env, isevars |- <pred> Cases tomatch of mat end - - where tomatch is some sequence of "instructions" (t1 ... tn) - - and mat is some matrix - (p11 ... p1n -> rhs1) - ( ... ) - (pm1 ... pmn -> rhsm) - - Terms to match: there are 3 kinds of instructions - - - "Pushed" terms to match are typed in [env]; these are usually just - Rel(n) except for the initial terms given by user and typed in [env] - - "Abstract" instructions means an abstraction has to be inserted in the - current branch to build (this means a pattern has been detected dependent - in another one and generalisation is necessary to ensure well-typing) - - "Alias" instructions means an alias has to be inserted (this alias - is usually removed at the end, except when its type is not the - same as the type of the matched term from which it comes - - typically because the inductive types are "real" parameters) - - Right-hand-sides: - - They consist of a raw term to type in an environment specific to the - clause they belong to: the names of declarations are those of the - variables present in the patterns. Therefore, they come with their - own [rhs_env] (actually it is the same as [env] except for the names - of variables). - -*) -type pattern_matching_problem = - { env : env; - isevars : Evd.evar_map ref; - pred : predicate_signature option; - tomatch : tomatch_stack; - history : pattern_continuation; - mat : matrix; - caseloc : loc; - casestyle: case_style; - typing_function: type_constraint -> env -> glob_constr -> unsafe_judgment } - -(*--------------------------------------------------------------------------* - * A few functions to infer the inductive type from the patterns instead of * - * checking that the patterns correspond to the ind. type of the * - * destructurated object. Allows type inference of examples like * - * match n with O => true | _ => false end * - * match x in I with C => true | _ => false end * - *--------------------------------------------------------------------------*) - -(* Computing the inductive type from the matrix of patterns *) - -(* We use the "in I" clause to coerce the terms to match and otherwise - use the constructor to know in which type is the matching problem - - Note that insertion of coercions inside nested patterns is done - each time the matrix is expanded *) - -let rec find_row_ind = function - [] -> None - | PatVar _ :: l -> find_row_ind l - | PatCstr(loc,c,_,_) :: _ -> Some (loc,c) - -let inductive_template isevars env tmloc ind = - let arsign = get_full_arity_sign env ind in - let hole_source = match tmloc with - | Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (ind,i)) - | None -> fun _ -> (dummy_loc, Evd.InternalHole) in - let (_,evarl,_) = - List.fold_right - (fun (na,b,ty) (subst,evarl,n) -> - match b with - | None -> - let ty' = substl subst ty in - let e = e_new_evar isevars env ~src:(hole_source n) ty' in - (e::subst,e::evarl,n+1) - | Some b -> - (b::subst,evarl,n+1)) - arsign ([],[],1) in - applist (mkInd ind,List.rev evarl) - - -(************************************************************************) -(* Utils *) - -let mkExistential env ?(src=(dummy_loc,Evd.InternalHole)) isevars = - e_new_evar isevars env ~src:src (new_Type ()) - -let evd_comb2 f isevars x y = - let (evd',y) = f !isevars x y in - isevars := evd'; - y - -let context_of_arsign l = - let (x, _) = List.fold_right - (fun c (x, n) -> - (lift_rel_context n c @ x, List.length c + n)) - l ([], 0) - in x - -(* We put the tycon inside the arity signature, possibly discovering dependencies. *) - -let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c = - let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in - let subst, len = - List.fold_left2 (fun (subst, len) (tm, tmtype) sign -> - let signlen = List.length sign in - match kind_of_term tm with - | Rel n when dependent tm c - && signlen = 1 (* The term to match is not of a dependent type itself *) -> - ((n, len) :: subst, len - signlen) - | Rel n when signlen > 1 (* The term is of a dependent type, - maybe some variable in its type appears in the tycon. *) -> - (match tmtype with - | NotInd _ -> (* len - signlen, subst*) assert false (* signlen > 1 *) - | IsInd (_, IndType(indf,realargs)) -> - let subst = - if dependent tm c && List.for_all isRel realargs - then (n, 1) :: subst else subst - in - List.fold_left - (fun (subst, len) arg -> - match kind_of_term arg with - | Rel n when dependent arg c -> - ((n, len) :: subst, pred len) - | _ -> (subst, pred len)) - (subst, len) realargs) - | _ -> (subst, len - signlen)) - ([], nar) tomatchs arsign - in - let rec predicate lift c = - match kind_of_term c with - | Rel n when n > lift -> - (try - (* Make the predicate dependent on the matched variable *) - let idx = List.assoc (n - lift) subst in - mkRel (idx + lift) - with Not_found -> - (* A variable that is not matched, lift over the arsign. *) - mkRel (n + nar)) - | _ -> - map_constr_with_binders succ predicate lift c - in - try - (* The tycon may be ill-typed after abstraction. *) - let pred = predicate 0 c in - let env' = push_rel_context (context_of_arsign arsign) env in - ignore(Typing.sort_of env' evm pred); pred - with e when Errors.noncritical e -> lift nar c - -module Cases_F(Coercion : Coercion.S) : S = struct - -let inh_coerce_to_ind isevars env ty tyi = - let expected_typ = inductive_template isevars env None tyi in - (* devrait źtre indifférent d'exiger leq ou pas puisque pour - un inductif cela doit źtre égal *) - let _ = e_cumul env isevars expected_typ ty in () - -let unify_tomatch_with_patterns isevars env loc typ pats = - match find_row_ind pats with - | None -> NotInd (None,typ) - | Some (_,(ind,_)) -> - inh_coerce_to_ind isevars env typ ind; - try IsInd (typ,find_rectype env ( !isevars) typ) - with Not_found -> NotInd (None,typ) - -let find_tomatch_tycon isevars env loc = function - (* Try if some 'in I ...' is present and can be used as a constraint *) - | Some (_,ind,_,_) -> mk_tycon (inductive_template isevars env loc ind) - | None -> empty_tycon - -let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) = - let loc = Some (loc_of_glob_constr tomatch) in - let tycon = find_tomatch_tycon isevars env loc indopt in - let j = typing_fun tycon env tomatch in - let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !isevars j in - isevars := evd; - let typ = nf_evar ( !isevars) j.uj_type in - let t = - try IsInd (typ,find_rectype env ( !isevars) typ) - with Not_found -> - unify_tomatch_with_patterns isevars env loc typ pats in - (j.uj_val,t) - -let coerce_to_indtype typing_fun isevars env matx tomatchl = - let pats = List.map (fun r -> r.patterns) matx in - let matx' = match matrix_transpose pats with - | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *) - | m -> m in - List.map2 (coerce_row typing_fun isevars env) matx' tomatchl - - - -let adjust_tomatch_to_pattern pb ((current,typ),deps) = - (* Ideally, we could find a common inductive type to which both the - term to match and the patterns coerce *) - (* In practice, we coerce the term to match if it is not already an - inductive type and it is not dependent; moreover, we use only - the first pattern type and forget about the others *) - let typ = match typ with IsInd (t,_) -> t | NotInd (_,t) -> t in - let typ = - try IsInd (typ,find_rectype pb.env ( !(pb.isevars)) typ) - with Not_found -> NotInd (None,typ) in - let tomatch = ((current,typ),deps) in - match typ with - | NotInd (None,typ) -> - let tm1 = List.map (fun eqn -> List.hd eqn.patterns) pb.mat in - (match find_row_ind tm1 with - | None -> tomatch - | Some (_,(ind,_)) -> - let indt = inductive_template pb.isevars pb.env None ind in - let current = - if deps = [] & isEvar typ then - (* Don't insert coercions if dependent; only solve evars *) - let _ = e_cumul pb.env pb.isevars indt typ in - current - else - (evd_comb2 (Coercion.inh_conv_coerce_to true dummy_loc pb.env) - pb.isevars (make_judge current typ) (mk_tycon_type indt)).uj_val in - let sigma = !(pb.isevars) in - let typ = IsInd (indt,find_rectype pb.env sigma indt) in - ((current,typ),deps)) - | _ -> tomatch - - (* extract some ind from [t], possibly coercing from constructors in [tm] *) -let to_mutind env isevars tm c t = -(* match c with - | Some body -> *) NotInd (c,t) -(* | None -> unify_tomatch_with_patterns isevars env t tm*) - -let type_of_tomatch = function - | IsInd (t,_) -> t - | NotInd (_,t) -> t - -let mkDeclTomatch na = function - | IsInd (t,_) -> (na,None,t) - | NotInd (c,t) -> (na,c,t) - -let map_tomatch_type f = function - | IsInd (t,ind) -> IsInd (f t,map_inductive_type f ind) - | NotInd (c,t) -> NotInd (Option.map f c, f t) - -let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth) -let lift_tomatch_type n = liftn_tomatch_type n 1 - -(**********************************************************************) -(* Utilities on patterns *) - -let current_pattern eqn = - match eqn.patterns with - | pat::_ -> pat - | [] -> anomaly "Empty list of patterns" - -let alias_of_pat = function - | PatVar (_,name) -> name - | PatCstr(_,_,_,name) -> name - -let remove_current_pattern eqn = - match eqn.patterns with - | pat::pats -> - { eqn with - patterns = pats; - alias_stack = alias_of_pat pat :: eqn.alias_stack } - | [] -> anomaly "Empty list of patterns" - -let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns } - -(**********************************************************************) -(* Well-formedness tests *) -(* Partial check on patterns *) - -exception NotAdjustable - -let rec adjust_local_defs loc = function - | (pat :: pats, (_,None,_) :: decls) -> - pat :: adjust_local_defs loc (pats,decls) - | (pats, (_,Some _,_) :: decls) -> - PatVar (loc, Anonymous) :: adjust_local_defs loc (pats,decls) - | [], [] -> [] - | _ -> raise NotAdjustable - -let check_and_adjust_constructor env ind cstrs = function - | PatVar _ as pat -> pat - | PatCstr (loc,((_,i) as cstr),args,alias) as pat -> - (* Check it is constructor of the right type *) - let ind' = inductive_of_constructor cstr in - if Names.eq_ind ind' ind then - (* Check the constructor has the right number of args *) - let ci = cstrs.(i-1) in - let nb_args_constr = ci.cs_nargs in - if List.length args = nb_args_constr then pat - else - try - let args' = adjust_local_defs loc (args, List.rev ci.cs_args) - in PatCstr (loc, cstr, args', alias) - with NotAdjustable -> - error_wrong_numarg_constructor_loc loc (Global.env()) - cstr nb_args_constr - else - (* Try to insert a coercion *) - try - Coercion.inh_pattern_coerce_to loc pat ind' ind - with Not_found -> - error_bad_constructor_loc loc cstr ind - -let check_all_variables typ mat = - List.iter - (fun eqn -> match current_pattern eqn with - | PatVar (_,id) -> () - | PatCstr (loc,cstr_sp,_,_) -> - error_bad_pattern_loc loc cstr_sp typ) - mat - -let check_unused_pattern env eqn = - if not !(eqn.used) then - raise_pattern_matching_error - (eqn.eqn_loc, env, UnusedClause eqn.patterns) - -let set_used_pattern eqn = eqn.used := true - -let extract_rhs pb = - match pb.mat with - | [] -> errorlabstrm "build_leaf" (mssg_may_need_inversion()) - | eqn::_ -> - set_used_pattern eqn; - eqn.rhs - -(**********************************************************************) -(* Functions to deal with matrix factorization *) - -let occur_in_rhs na rhs = - match na with - | Anonymous -> false - | Name id -> occur_glob_constr id rhs.it - -let is_dep_patt eqn = function - | PatVar (_,name) -> occur_in_rhs name eqn.rhs - | PatCstr _ -> true - -let dependencies_in_rhs nargs eqns = - if eqns = [] then list_tabulate (fun _ -> false) nargs (* Only "_" patts *) - else - let deps = List.map (fun (tms,eqn) -> List.map (is_dep_patt eqn) tms) eqns in - let columns = matrix_transpose deps in - List.map (List.exists ((=) true)) columns - -let dependent_decl a = function - | (na,None,t) -> dependent a t - | (na,Some c,t) -> dependent a t || dependent a c - -(* Computing the matrix of dependencies *) - -(* We are in context d1...dn |- and [find_dependencies k 1 nextlist] - computes for declaration [k+1] in which of declarations in - [nextlist] (which corresponds to d(k+2)...dn) it depends; - declarations are expressed by index, e.g. in dependency list - [n-2;1], [1] points to [dn] and [n-2] to [d3] *) - -let rec find_dependency_list k n = function - | [] -> [] - | (used,tdeps,d)::rest -> - let deps = find_dependency_list k (n+1) rest in - if used && dependent_decl (mkRel n) d - then list_add_set (List.length rest + 1) (list_union deps tdeps) - else deps - -let find_dependencies is_dep_or_cstr_in_rhs d (k,nextlist) = - let deps = find_dependency_list k 1 nextlist in - if is_dep_or_cstr_in_rhs || deps <> [] - then (k-1,(true ,deps,d)::nextlist) - else (k-1,(false,[] ,d)::nextlist) - -let find_dependencies_signature deps_in_rhs typs = - let k = List.length deps_in_rhs in - let _,l = List.fold_right2 find_dependencies deps_in_rhs typs (k,[]) in - List.map (fun (_,deps,_) -> deps) l - -(******) - -(* A Pushed term to match has just been substituted by some - constructor t = (ci x1...xn) and the terms x1 ... xn have been added to - match - - - all terms to match and to push (dependent on t by definition) - must have (Rel depth) substituted by t and Rel's>depth lifted by n - - all pushed terms to match (non dependent on t by definition) must - be lifted by n - - We start with depth=1 -*) - -let regeneralize_index_tomatch n = - let rec genrec depth = function - | [] -> [] - | Pushed ((c,tm),l)::rest -> - let c = regeneralize_index n depth c in - let tm = map_tomatch_type (regeneralize_index n depth) tm in - let l = List.map (regeneralize_rel n depth) l in - Pushed ((c,tm),l)::(genrec depth rest) - | Alias (c1,c2,d,t)::rest -> - Alias (regeneralize_index n depth c1,c2,d,t)::(genrec depth rest) - | Abstract d::rest -> - Abstract (map_rel_declaration (regeneralize_index n depth) d) - ::(genrec (depth+1) rest) in - genrec 0 - -let rec replace_term n c k t = - if isRel t && destRel t = n+k then lift k c - else map_constr_with_binders succ (replace_term n c) k t - -let replace_tomatch n c = - let rec replrec depth = function - | [] -> [] - | Pushed ((b,tm),l)::rest -> - let b = replace_term n c depth b in - let tm = map_tomatch_type (replace_term n c depth) tm in - List.iter (fun i -> if i=n+depth then anomaly "replace_tomatch") l; - Pushed ((b,tm),l)::(replrec depth rest) - | Alias (c1,c2,d,t)::rest -> - Alias (replace_term n c depth c1,c2,d,t)::(replrec depth rest) - | Abstract d::rest -> - Abstract (map_rel_declaration (replace_term n c depth) d) - ::(replrec (depth+1) rest) in - replrec 0 - -let rec liftn_tomatch_stack n depth = function - | [] -> [] - | Pushed ((c,tm),l)::rest -> - let c = liftn n depth c in - let tm = liftn_tomatch_type n depth tm in - let l = List.map (fun i -> if i<depth then i else i+n) l in - Pushed ((c,tm),l)::(liftn_tomatch_stack n depth rest) - | Alias (c1,c2,d,t)::rest -> - Alias (liftn n depth c1,liftn n depth c2,d,liftn n depth t) - ::(liftn_tomatch_stack n depth rest) - | Abstract d::rest -> - Abstract (map_rel_declaration (liftn n depth) d) - ::(liftn_tomatch_stack n (depth+1) rest) - - -let lift_tomatch_stack n = liftn_tomatch_stack n 1 - -(* if [current] has type [I(p1...pn u1...um)] and we consider the case - of constructor [ci] of type [I(p1...pn u'1...u'm)], then the - default variable [name] is expected to have which type? - Rem: [current] is [(Rel i)] except perhaps for initial terms to match *) - -(************************************************************************) -(* Some heuristics to get names for variables pushed in pb environment *) -(* Typical requirement: - - [match y with (S (S x)) => x | x => x end] should be compiled into - [match y with O => y | (S n) => match n with O => y | (S x) => x end end] - - and [match y with (S (S n)) => n | n => n end] into - [match y with O => y | (S n0) => match n0 with O => y | (S n) => n end end] - - i.e. user names should be preserved and created names should not - interfere with user names *) - -let merge_name get_name obj = function - | Anonymous -> get_name obj - | na -> na - -let merge_names get_name = List.map2 (merge_name get_name) - -let get_names env sign eqns = - let names1 = list_tabulate (fun _ -> Anonymous) (List.length sign) in - (* If any, we prefer names used in pats, from top to bottom *) - let names2 = - List.fold_right - (fun (pats,eqn) names -> merge_names alias_of_pat pats names) - eqns names1 in - (* Otherwise, we take names from the parameters of the constructor but - avoiding conflicts with user ids *) - let allvars = - List.fold_left (fun l (_,eqn) -> list_union l eqn.rhs.avoid_ids) [] eqns in - let names4,_ = - List.fold_left2 - (fun (l,avoid) d na -> - let na = - merge_name - (fun (na,_,t) -> Name (next_name_away (named_hd env t na) avoid)) - d na - in - (na::l,(out_name na)::avoid)) - ([],allvars) (List.rev sign) names2 in - names4 - -(************************************************************************) -(* Recovering names for variables pushed to the rhs' environment *) - -let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t)) - -let all_name sign = List.map (fun (n, b, t) -> let n = match n with Name _ -> n | Anonymous -> Name (id_of_string "Anonymous") in - (n, b, t)) sign - -let push_rels_eqn sign eqn = - let sign = all_name sign in - {eqn with rhs = {eqn.rhs with rhs_env = push_rels sign eqn.rhs.rhs_env; } } - -let push_rels_eqn_with_names sign eqn = - let pats = List.rev (list_firstn (List.length sign) eqn.patterns) in - let sign = recover_alias_names alias_of_pat pats sign in - push_rels_eqn sign eqn - -let build_aliases_context env sigma names allpats pats = - (* pats is the list of bodies to push as an alias *) - (* They all are defined in env and we turn them into a sign *) - (* cuts in sign need to be done in allpats *) - let rec insert env sign1 sign2 n newallpats oldallpats = function - | (deppat,_,_,_)::pats, Anonymous::names when not (isRel deppat) -> - (* Anonymous leaves must be considered named and treated in the *) - (* next clause because they may occur in implicit arguments *) - insert env sign1 sign2 - n newallpats (List.map List.tl oldallpats) (pats,names) - | (deppat,nondeppat,d,t)::pats, na::names -> - let nondeppat = lift n nondeppat in - let deppat = lift n deppat in - let newallpats = - List.map2 (fun l1 l2 -> List.hd l2::l1) newallpats oldallpats in - let oldallpats = List.map List.tl oldallpats in - let decl = (na,Some deppat,t) in - let a = (deppat,nondeppat,d,t) in - insert (push_rel decl env) (decl::sign1) ((na,a)::sign2) (n+1) - newallpats oldallpats (pats,names) - | [], [] -> newallpats, sign1, sign2, env - | _ -> anomaly "Inconsistent alias and name lists" in - let allpats = List.map (fun x -> [x]) allpats - in insert env [] [] 0 (List.map (fun _ -> []) allpats) allpats (pats, names) - -let insert_aliases_eqn sign eqnnames alias_rest eqn = - let thissign = List.map2 (fun na (_,c,t) -> (na,c,t)) eqnnames sign in - push_rels_eqn thissign { eqn with alias_stack = alias_rest; } - - -let insert_aliases env sigma alias eqns = - (* Lą, y a une faiblesse, si un alias est utilisé dans un cas par *) - (* défaut présent mais inutile, ce qui est le cas général, l'alias *) - (* est introduit mźme s'il n'est pas utilisé dans les cas réguliers *) - let eqnsnames = List.map (fun eqn -> List.hd eqn.alias_stack) eqns in - let alias_rests = List.map (fun eqn -> List.tl eqn.alias_stack) eqns in - (* names2 takes the meet of all needed aliases *) - let names2 = - List.fold_right (merge_name (fun x -> x)) eqnsnames Anonymous in - (* Only needed aliases are kept by build_aliases_context *) - let eqnsnames, sign1, sign2, env = - build_aliases_context env sigma [names2] eqnsnames [alias] in - let eqns = list_map3 (insert_aliases_eqn sign1) eqnsnames alias_rests eqns in - sign2, env, eqns - -(**********************************************************************) -(* Functions to deal with elimination predicate *) - -exception Occur -let noccur_between_without_evar n m term = - let rec occur_rec n c = match kind_of_term c with - | Rel p -> if n<=p && p<n+m then raise Occur - | Evar (_,cl) -> () - | _ -> iter_constr_with_binders succ occur_rec n c - in - try occur_rec n term; true with Occur -> false - -(* Inferring the predicate *) -let prepare_unif_pb typ cs = - let n = List.length (assums_of_rel_context cs.cs_args) in - - (* We may need to invert ci if its parameters occur in typ *) - let typ' = - if noccur_between_without_evar 1 n typ then lift (-n) typ - else (* TODO4-1 *) - error "Unable to infer return clause of this pattern-matching problem" in - let args = extended_rel_list (-n) cs.cs_args in - let ci = applist (mkConstruct cs.cs_cstr, cs.cs_params@args) in - - (* This is the problem: finding P s.t. cs_args |- (P realargs ci) = typ' *) - (Array.map (lift (-n)) cs.cs_concl_realargs, ci, typ') - - -(* Infering the predicate *) -(* -The problem to solve is the following: - -We match Gamma |- t : I(u01..u0q) against the following constructors: - - Gamma, x11...x1p1 |- C1(x11..x1p1) : I(u11..u1q) - ... - Gamma, xn1...xnpn |- Cn(xn1..xnp1) : I(un1..unq) - -Assume the types in the branches are the following - - Gamma, x11...x1p1 |- branch1 : T1 - ... - Gamma, xn1...xnpn |- branchn : Tn - -Assume the type of the global case expression is Gamma |- T - -The predicate has the form phi = [y1..yq][z:I(y1..yq)]? and must satisfy -the following n+1 equations: - - Gamma, x11...x1p1 |- (phi u11..u1q (C1 x11..x1p1)) = T1 - ... - Gamma, xn1...xnpn |- (phi un1..unq (Cn xn1..xnpn)) = Tn - Gamma |- (phi u01..u0q t) = T - -Some hints: - -- Clearly, if xij occurs in Ti, then, a "match z with (Ci xi1..xipi) => ..." - should be inserted somewhere in Ti. - -- If T is undefined, an easy solution is to insert a "match z with (Ci - xi1..xipi) => ..." in front of each Ti - -- Otherwise, T1..Tn and T must be step by step unified, if some of them - diverge, then try to replace the diverging subterm by one of y1..yq or z. - -- The main problem is what to do when an existential variables is encountered - -let prepare_unif_pb typ cs = - let n = cs.cs_nargs in - let _,p = decompose_prod_n n typ in - let ci = build_dependent_constructor cs in - (* This is the problem: finding P s.t. cs_args |- (P realargs ci) = p *) - (n, cs.cs_concl_realargs, ci, p) - -let eq_operator_lift k (n,n') = function - | OpRel p, OpRel p' when p > k & p' > k -> - if p < k+n or p' < k+n' then false else p - n = p' - n' - | op, op' -> op = op' - -let rec transpose_args n = - if n=0 then [] - else - (Array.map (fun l -> List.hd l) lv):: - (transpose_args (m-1) (Array.init (fun l -> List.tl l))) - -let shift_operator k = function OpLambda _ | OpProd _ -> k+1 | _ -> k - -let reloc_operator (k,n) = function OpRel p when p > k -> -let rec unify_clauses k pv = - let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) ( isevars)) p) pv in - let n1,op1 = let (n1,(op1,args1)) = pv'.(0) in n1,op1 in - if Array.for_all (fun (ni,(opi,_)) -> eq_operator_lift k (n1,ni) (op1,opi)) pv' - then - let argvl = transpose_args (List.length args1) pv' in - let k' = shift_operator k op1 in - let argl = List.map (unify_clauses k') argvl in - gather_constr (reloc_operator (k,n1) op1) argl -*) - -let abstract_conclusion typ cs = - let n = List.length (assums_of_rel_context cs.cs_args) in - let (sign,p) = decompose_prod_n n typ in - it_mkLambda p sign - -let infer_predicate loc env isevars typs cstrs indf = - (* Il faudra substituer les isevars a un certain moment *) - if Array.length cstrs = 0 then (* "TODO4-3" *) - error "Inference of annotation for empty inductive types not implemented" - else - (* Empiric normalization: p may depend in a irrelevant way on args of the*) - (* cstr as in [c:{_:Alpha & Beta}] match c with (existS a b)=>(a,b) end *) - let typs = - Array.map (local_strong whd_beta ( !isevars)) typs - in - let eqns = array_map2 prepare_unif_pb typs cstrs in - (* First strategy: no dependencies at all *) -(* - let (mis,_) = dest_ind_family indf in - let (cclargs,_,typn) = eqns.(mis_nconstr mis -1) in -*) - let (sign,_) = get_arity env indf in - let mtyp = - if array_exists is_Type typs then - (* Heuristic to avoid comparison between non-variables algebric univs*) - new_Type () - else - mkExistential env ~src:(loc, Evd.CasesType) isevars - in - if array_for_all (fun (_,_,typ) -> e_cumul env isevars typ mtyp) eqns - then - (* Non dependent case -> turn it into a (dummy) dependent one *) - let sign = (Anonymous,None,build_dependent_inductive env indf)::sign in - let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in - (true,pred) (* true = dependent -- par défaut *) - else -(* - let s = get_sort_of env ( isevars) typs.(0) in - let predpred = it_mkLambda_or_LetIn (mkSort s) sign in - let caseinfo = make_default_case_info mis in - let brs = array_map2 abstract_conclusion typs cstrs in - let predbody = mkCase (caseinfo, (nf_betaiota predpred), mkRel 1, brs) in - let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in -*) - (* "TODO4-2" *) - (* We skip parameters *) - let cis = - Array.map - (fun cs -> - applist (mkConstruct cs.cs_cstr, extended_rel_list 0 cs.cs_args)) - cstrs in - let ct = array_map2 (fun ci (_,_,t) -> (ci,t)) cis eqns in - raise_pattern_matching_error (loc,env, CannotInferPredicate ct) -(* - (true,pred) -*) - -(* Propagation of user-provided predicate through compilation steps *) - -let rec map_predicate f k = function - | PrCcl ccl -> PrCcl (f k ccl) - | PrProd pred -> - PrProd (map_predicate f (k+1) pred) - | PrLetIn ((names,dep as tm),pred) -> - let k' = List.length names + (if dep<>Anonymous then 1 else 0) in - PrLetIn (tm, map_predicate f (k+k') pred) - -let rec noccurn_predicate k = function - | PrCcl ccl -> noccurn k ccl - | PrProd pred -> noccurn_predicate (k+1) pred - | PrLetIn ((names,dep),pred) -> - let k' = List.length names + (if dep<>Anonymous then 1 else 0) in - noccurn_predicate (k+k') pred - -let liftn_predicate n = map_predicate (liftn n) - -let lift_predicate n = liftn_predicate n 1 - -let regeneralize_index_predicate n = map_predicate (regeneralize_index n) 0 - -let substnl_predicate sigma = map_predicate (substnl sigma) - -(* This is parallel bindings *) -let subst_predicate (args,copt) pred = - let sigma = match copt with - | None -> List.rev args - | Some c -> c::(List.rev args) in - substnl_predicate sigma 0 pred - -let specialize_predicate_var (cur,typ) = function - | PrProd _ | PrCcl _ -> - anomaly "specialize_predicate_var: a pattern-variable must be pushed" - | PrLetIn (([],dep),pred) -> - subst_predicate ([],if dep<>Anonymous then Some cur else None) pred - | PrLetIn ((_,dep),pred) -> - (match typ with - | IsInd (_,IndType (_,realargs)) -> - subst_predicate (realargs,if dep<>Anonymous then Some cur else None) pred - | _ -> anomaly "specialize_predicate_var") - -let ungeneralize_predicate = function - | PrLetIn _ | PrCcl _ -> anomaly "ungeneralize_predicate: expects a product" - | PrProd pred -> pred - -(*****************************************************************************) -(* We have pred = [X:=realargs;x:=c]P typed in Gamma1, x:I(realargs), Gamma2 *) -(* and we want to abstract P over y:t(x) typed in the same context to get *) -(* *) -(* pred' = [X:=realargs;x':=c](y':t(x'))P[y:=y'] *) -(* *) -(* We first need to lift t(x) s.t. it is typed in Gamma, X:=rargs, x' *) -(* then we have to replace x by x' in t(x) and y by y' in P *) -(*****************************************************************************) -let generalize_predicate ny d = function - | PrLetIn ((names,dep as tm),pred) -> - if dep=Anonymous then anomaly "Undetected dependency"; - let p = List.length names + 1 in - let pred = lift_predicate 1 pred in - let pred = regeneralize_index_predicate (ny+p+1) pred in - PrLetIn (tm, PrProd pred) - | PrProd _ | PrCcl _ -> - anomaly "generalize_predicate: expects a non trivial pattern" - -let rec extract_predicate l = function - | pred, Alias (deppat,nondeppat,_,_)::tms -> - let tms' = match kind_of_term nondeppat with - | Rel i -> replace_tomatch i deppat tms - | _ -> (* initial terms are not dependent *) tms in - extract_predicate l (pred,tms') - | PrProd pred, Abstract d'::tms -> - let d' = map_rel_declaration (lift (List.length l)) d' in - substl l (mkProd_or_LetIn d' (extract_predicate [] (pred,tms))) - | PrLetIn (([],dep),pred), Pushed ((cur,_),_)::tms -> - extract_predicate (if dep<>Anonymous then cur::l else l) (pred,tms) - | PrLetIn ((_,dep),pred), Pushed ((cur,IsInd (_,(IndType(_,realargs)))),_)::tms -> - let l = List.rev realargs@l in - extract_predicate (if dep<>Anonymous then cur::l else l) (pred,tms) - | PrCcl ccl, [] -> - substl l ccl - | _ -> anomaly"extract_predicate: predicate inconsistent with terms to match" - -let abstract_predicate env sigma indf cur tms = function - | (PrProd _ | PrCcl _) -> anomaly "abstract_predicate: must be some LetIn" - | PrLetIn ((names,dep),pred) -> - let sign = make_arity_signature env true indf in - (* n is the number of real args + 1 *) - let n = List.length sign in - let tms = lift_tomatch_stack n tms in - let tms = - match kind_of_term cur with - | Rel i -> regeneralize_index_tomatch (i+n) tms - | _ -> (* Initial case *) tms in - (* Depending on whether the predicate is dependent or not, and has real - args or not, we lift it to make room for [sign] *) - (* Even if not intrinsically dep, we move the predicate into a dep one *) - let sign,k = - if names = [] & n <> 1 then - (* Real args were not considered *) - (if dep<>Anonymous then - ((let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign),n-1) - else - (sign,n)) - else - (* Real args are OK *) - (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign, - if dep<>Anonymous then 0 else 1) in - let pred = lift_predicate k pred in - let pred = extract_predicate [] (pred,tms) in - (true, it_mkLambda_or_LetIn_name env pred sign) - -let rec known_dependent = function - | None -> false - | Some (PrLetIn ((_,dep),_)) -> dep<>Anonymous - | Some (PrCcl _) -> false - | Some (PrProd _) -> - anomaly "known_dependent: can only be used when patterns remain" - -(* [expand_arg] is used by [specialize_predicate] - it replaces gamma, x1...xn, x1...xk |- pred - by gamma, x1...xn, x1...xk-1 |- [X=realargs,xk=xk]pred (if dep) or - by gamma, x1...xn, x1...xk-1 |- [X=realargs]pred (if not dep) *) - -let expand_arg n alreadydep (na,t) deps (k,pred) = - (* current can occur in pred even if the original problem is not dependent *) - let dep = - if alreadydep<>Anonymous then alreadydep - else if deps = [] && noccurn_predicate 1 pred then Anonymous - else Name (id_of_string "x") in - let pred = if dep<>Anonymous then pred else lift_predicate (-1) pred in - (* There is no dependency in realargs for subpattern *) - (k-1, PrLetIn (([],dep), pred)) - - -(*****************************************************************************) -(* pred = [X:=realargs;x:=c]P types the following problem: *) -(* *) -(* Gamma |- match Pushed(c:I(realargs)) rest with...end: pred *) -(* *) -(* where the branch with constructor Ci:(x1:T1)...(xn:Tn)->I(realargsi) *) -(* is considered. Assume each Ti is some Ii(argsi). *) -(* We let e=Ci(x1,...,xn) and replace pred by *) -(* *) -(* pred' = [X1:=rargs1,x1:=x1']...[Xn:=rargsn,xn:=xn'](P[X:=realargsi;x:=e]) *) -(* *) -(* s.t Gamma,x1'..xn' |- match Pushed(x1')..Pushed(xn') rest with..end :pred'*) -(* *) -(*****************************************************************************) -let specialize_predicate tomatchs deps cs = function - | (PrProd _ | PrCcl _) -> - anomaly "specialize_predicate: a matched pattern must be pushed" - | PrLetIn ((names,isdep),pred) -> - (* Assume some gamma st: gamma, (X,x:=realargs,copt) |- pred *) - let nrealargs = List.length names in - let k = nrealargs + (if isdep<>Anonymous then 1 else 0) in - (* We adjust pred st: gamma, x1..xn, (X,x:=realargs,copt) |- pred' *) - let n = cs.cs_nargs in - let pred' = liftn_predicate n (k+1) pred in - let argsi = if nrealargs <> 0 then Array.to_list cs.cs_concl_realargs else [] in - let copti = if isdep<>Anonymous then Some (build_dependent_constructor cs) else None in - (* The substituends argsi, copti are all defined in gamma, x1...xn *) - (* We need _parallel_ bindings to get gamma, x1...xn |- pred'' *) - let pred'' = subst_predicate (argsi, copti) pred' in - (* We adjust pred st: gamma, x1..xn, x1..xn |- pred'' *) - let pred''' = liftn_predicate n (n+1) pred'' in - (* We finally get gamma,x1..xn |- [X1,x1:=R1,x1]..[Xn,xn:=Rn,xn]pred'''*) - snd (List.fold_right2 (expand_arg n isdep) tomatchs deps (n,pred''')) - -let find_predicate loc env isevars p typs cstrs current - (IndType (indf,realargs)) tms = - let (dep,pred) = - match p with - | Some p -> abstract_predicate env ( !isevars) indf current tms p - | None -> infer_predicate loc env isevars typs cstrs indf in - let typ = whd_beta ( !isevars) (applist (pred, realargs)) in - if dep then - (pred, whd_beta ( !isevars) (applist (typ, [current])), - new_Type ()) - else - (pred, typ, new_Type ()) - -(************************************************************************) -(* Sorting equations by constructor *) - -type inversion_problem = - (* the discriminating arg in some Ind and its order in Ind *) - | Incompatible of int * (int * int) - | Constraints of (int * constr) list - -let solve_constraints constr_info indt = - (* TODO *) - Constraints [] - -let rec irrefutable env = function - | PatVar (_,name) -> true - | PatCstr (_,cstr,args,_) -> - let ind = inductive_of_constructor cstr in - let (_,mip) = Inductive.lookup_mind_specif env ind in - let one_constr = Array.length mip.mind_user_lc = 1 in - one_constr & List.for_all (irrefutable env) args - -let first_clause_irrefutable env = function - | eqn::mat -> List.for_all (irrefutable env) eqn.patterns - | _ -> false - -let group_equations pb ind current cstrs mat = - let mat = - if first_clause_irrefutable pb.env mat then [List.hd mat] else mat in - let brs = Array.create (Array.length cstrs) [] in - let only_default = ref true in - let _ = - List.fold_right (* To be sure it's from bottom to top *) - (fun eqn () -> - let rest = remove_current_pattern eqn in - let pat = current_pattern eqn in - match check_and_adjust_constructor pb.env ind cstrs pat with - | PatVar (_,name) -> - (* This is a default clause that we expand *) - for i=1 to Array.length cstrs do - let n = cstrs.(i-1).cs_nargs in - let args = make_anonymous_patvars n in - brs.(i-1) <- (args, rest) :: brs.(i-1) - done - | PatCstr (loc,((_,i)),args,_) -> - (* This is a regular clause *) - only_default := false; - brs.(i-1) <- (args,rest) :: brs.(i-1)) mat () in - (brs,!only_default) - -(************************************************************************) -(* Here starts the pattern-matching compilation algorithm *) - -(* Abstracting over dependent subterms to match *) -let rec generalize_problem pb = function - | [] -> pb - | i::l -> - let d = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in - let pb' = generalize_problem pb l in - let tomatch = lift_tomatch_stack 1 pb'.tomatch in - let tomatch = regeneralize_index_tomatch (i+1) tomatch in - { pb with - tomatch = Abstract d :: tomatch; - pred = Option.map (generalize_predicate i d) pb'.pred } - -(* No more patterns: typing the right-hand side of equations *) -let build_leaf pb = - let rhs = extract_rhs pb in - let tycon = match pb.pred with - | None -> anomaly "Predicate not found" - | Some (PrCcl typ) -> mk_tycon typ - | Some _ -> anomaly "not all parameters of pred have been consumed" in - pb.typing_function tycon rhs.rhs_env rhs.it - -(* Building the sub-problem when all patterns are variables *) -let shift_problem (current,t) pb = - {pb with - tomatch = Alias (current,current,NonDepAlias,type_of_tomatch t)::pb.tomatch; - pred = Option.map (specialize_predicate_var (current,t)) pb.pred; - history = push_history_pattern 0 AliasLeaf pb.history; - mat = List.map remove_current_pattern pb.mat } - -(* Building the sub-pattern-matching problem for a given branch *) -let build_branch current deps pb eqns const_info = - (* We remember that we descend through a constructor *) - let alias_type = - if Array.length const_info.cs_concl_realargs = 0 - & not (known_dependent pb.pred) & deps = [] - then - NonDepAlias - else - DepAlias - in - let history = - push_history_pattern const_info.cs_nargs - (AliasConstructor const_info.cs_cstr) - pb.history in - - (* We find matching clauses *) - let cs_args = (*assums_of_rel_context*) const_info.cs_args in - let names = get_names pb.env cs_args eqns in - let submat = List.map (fun (tms,eqn) -> prepend_pattern tms eqn) eqns in - if submat = [] then - raise_pattern_matching_error - (dummy_loc, pb.env, NonExhaustive (complete_history history)); - let typs = List.map2 (fun (_,c,t) na -> (na,c,t)) cs_args names in - let _,typs',_ = - List.fold_right - (fun (na,c,t as d) (env,typs,tms) -> - let tm1 = List.map List.hd tms in - let tms = List.map List.tl tms in - (push_rel d env, (na,to_mutind env pb.isevars tm1 c t)::typs,tms)) - typs (pb.env,[],List.map fst eqns) in - - let dep_sign = - find_dependencies_signature - (dependencies_in_rhs const_info.cs_nargs eqns) (List.rev typs) in - - (* The dependent term to subst in the types of the remaining UnPushed - terms is relative to the current context enriched by topushs *) - let ci = build_dependent_constructor const_info in - - (* We replace [(mkRel 1)] by its expansion [ci] *) - (* and context "Gamma = Gamma1, current, Gamma2" by "Gamma;typs;curalias" *) - (* This is done in two steps : first from "Gamma |- tms" *) - (* into "Gamma; typs; curalias |- tms" *) - let tomatch = lift_tomatch_stack const_info.cs_nargs pb.tomatch in - - let currents = - list_map2_i - (fun i (na,t) deps -> Pushed ((mkRel i, lift_tomatch_type i t), deps)) - 1 typs' (List.rev dep_sign) in - - let sign = List.map (fun (na,t) -> mkDeclTomatch na t) typs' in - let ind = - appvect ( - applist (mkInd (inductive_of_constructor const_info.cs_cstr), - List.map (lift const_info.cs_nargs) const_info.cs_params), - const_info.cs_concl_realargs) in - - let cur_alias = lift (List.length sign) current in - let currents = Alias (ci,cur_alias,alias_type,ind) :: currents in - let env' = push_rels sign pb.env in - let pred' = Option.map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in - sign, - { pb with - env = env'; - tomatch = List.rev_append currents tomatch; - pred = pred'; - history = history; - mat = List.map (push_rels_eqn_with_names sign) submat } - -(********************************************************************** - INVARIANT: - - pb = { env, subst, tomatch, mat, ...} - tomatch = list of Pushed (c:T) or Abstract (na:T) or Alias (c:T) - - "Pushed" terms and types are relative to env - "Abstract" types are relative to env enriched by the previous terms to match - -*) - -(**********************************************************************) -(* Main compiling descent *) -let rec compile pb = - match pb.tomatch with - | (Pushed cur)::rest -> match_current { pb with tomatch = rest } cur - | (Alias x)::rest -> compile_alias pb x rest - | (Abstract d)::rest -> compile_generalization pb d rest - | [] -> build_leaf pb - -and match_current pb tomatch = - let ((current,typ as ct),deps) = adjust_tomatch_to_pattern pb tomatch in - match typ with - | NotInd (_,typ) -> - check_all_variables typ pb.mat; - compile (shift_problem ct pb) - | IsInd (_,(IndType(indf,realargs) as indt)) -> - let mind,_ = dest_ind_family indf in - let cstrs = get_constructors pb.env indf in - let eqns,onlydflt = group_equations pb mind current cstrs pb.mat in - if (Array.length cstrs <> 0 or pb.mat <> []) & onlydflt then - compile (shift_problem ct pb) - else - let _constraints = Array.map (solve_constraints indt) cstrs in - - (* We generalize over terms depending on current term to match *) - let pb = generalize_problem pb deps in - - (* We compile branches *) - let brs = array_map2 (compile_branch current deps pb) eqns cstrs in - - (* We build the (elementary) case analysis *) - let brvals = Array.map (fun (v,_) -> v) brs in - let brtyps = Array.map (fun (_,t) -> t) brs in - let (pred,typ,s) = - find_predicate pb.caseloc pb.env pb.isevars - pb.pred brtyps cstrs current indt pb.tomatch in - let ci = make_case_info pb.env mind pb.casestyle in - let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in - let inst = List.map mkRel deps in - { uj_val = applist (case, inst); - uj_type = substl inst typ } - -and compile_branch current deps pb eqn cstr = - let sign, pb = build_branch current deps pb eqn cstr in - let j = compile pb in - (it_mkLambda_or_LetIn j.uj_val sign, j.uj_type) - -and compile_generalization pb d rest = - let pb = - { pb with - env = push_rel d pb.env; - tomatch = rest; - pred = Option.map ungeneralize_predicate pb.pred; - mat = List.map (push_rels_eqn [d]) pb.mat } in - let j = compile pb in - { uj_val = mkLambda_or_LetIn d j.uj_val; - uj_type = mkProd_or_LetIn d j.uj_type } - -and compile_alias pb (deppat,nondeppat,d,t) rest = - let history = simplify_history pb.history in - let sign, newenv, mat = - insert_aliases pb.env ( !(pb.isevars)) (deppat,nondeppat,d,t) pb.mat in - let n = List.length sign in - - (* We had Gamma1; x:current; Gamma2 |- tomatch(x) and we rebind x to get *) - (* Gamma1; x:current; Gamma2; typs; x':=curalias |- tomatch(x') *) - let tomatch = lift_tomatch_stack n rest in - let tomatch = match kind_of_term nondeppat with - | Rel i -> - if n = 1 then regeneralize_index_tomatch (i+n) tomatch - else replace_tomatch i deppat tomatch - | _ -> (* initial terms are not dependent *) tomatch in - - let pb = - {pb with - env = newenv; - tomatch = tomatch; - pred = Option.map (lift_predicate n) pb.pred; - history = history; - mat = mat } in - let j = compile pb in - List.fold_left mkSpecialLetInJudge j sign - -(* pour les alias des initiaux, enrichir les env de ce qu'il faut et -substituer aprčs par les initiaux *) - -(**************************************************************************) -(* Preparation of the pattern-matching problem *) - -(* builds the matrix of equations testing that each eqn has n patterns - * and linearizing the _ patterns. - * Syntactic correctness has already been done in astterm *) -let matx_of_eqns env eqns = - let build_eqn (loc,ids,lpat,rhs) = - let rhs = - { rhs_env = env; - avoid_ids = ids@(ids_of_named_context (named_context env)); - it = rhs; - } in - { patterns = lpat; - alias_stack = []; - eqn_loc = loc; - used = ref false; - rhs = rhs } - in List.map build_eqn eqns - -(************************************************************************) -(* preparing the elimination predicate if any *) - -let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c = - let cook (n, l, env, signs) = function - | c,IsInd (_,IndType(indf,realargs)) -> - let indf' = lift_inductive_family n indf in - let sign = make_arity_signature env dep indf' in - let p = List.length realargs in - if dep then - (n + p + 1, c::(List.rev realargs)@l, push_rels sign env,sign::signs) - else - (n + p, (List.rev realargs)@l, push_rels sign env,sign::signs) - | c,NotInd _ -> - (n, l, env, []::signs) in - let n, allargs, env, signs = List.fold_left cook (0, [], env, []) tomatchs in - let names = List.rev (List.map (List.map pi1) signs) in - let allargs = - List.map (fun c -> lift n (nf_betadeltaiota env ( !isevars) c)) allargs in - let rec build_skeleton env c = - (* Don't put into normal form, it has effects on the synthesis of evars *) - (* let c = whd_betadeltaiota env ( isevars) c in *) - (* We turn all subterms possibly dependent into an evar with maximum ctxt*) - if isEvar c or List.exists (eq_constr c) allargs then - e_new_evar isevars env ~src:(loc, Evd.CasesType) - (Retyping.get_type_of env ( !isevars) c) - else - map_constr_with_full_binders push_rel build_skeleton env c - in - names, build_skeleton env (lift n c) - -(* Here, [pred] is assumed to be in the context built from all *) -(* realargs and terms to match *) -let build_initial_predicate isdep allnames pred = - let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in - let rec buildrec n pred = function - | [] -> PrCcl pred - | names::lnames -> - let names' = if isdep then List.tl names else names in - let n' = n + List.length names' in - let pred, p, user_p = - if isdep then - if dependent (mkRel (nar-n')) pred then pred, 1, 1 - else liftn (-1) (nar-n') pred, 0, 1 - else pred, 0, 0 in - let na = - if p=1 then - let na = List.hd names in - if na = Anonymous then - (* peut arriver en raison des evars *) - Name (id_of_string "x") (*Hum*) - else na - else Anonymous in - PrLetIn ((names',na), buildrec (n'+user_p) pred lnames) - in buildrec 0 pred allnames - -let extract_arity_signature env0 tomatchl tmsign = - let get_one_sign n tm (na,t) = - match tm with - | NotInd (bo,typ) -> - (match t with - | None -> [na,Option.map (lift n) bo,lift n typ] - | Some (loc,_,_,_) -> - user_err_loc (loc,"", - str "Unexpected type annotation for a term of non inductive type")) - | IsInd (_,IndType(indf,realargs)) -> - let indf' = lift_inductive_family n indf in - let (ind,params) = dest_ind_family indf' in - let nrealargs = List.length realargs in - let realnal = - match t with - | Some (loc,ind',nparams,realnal) -> - if ind <> ind' then - user_err_loc (loc,"",str "Wrong inductive type"); - if List.length params <> nparams - or nrealargs <> List.length realnal then - anomaly "Ill-formed 'in' clause in cases"; - List.rev realnal - | None -> list_tabulate (fun _ -> Anonymous) nrealargs in - let arsign = fst (get_arity env0 indf') in - (na,None,build_dependent_inductive env0 indf') - ::(List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign) in - let rec buildrec n = function - | [],[] -> [] - | (_,tm)::ltm, x::tmsign -> - let l = get_one_sign n tm x in - l :: buildrec (n + List.length l) (ltm,tmsign) - | _ -> assert false - in List.rev (buildrec 0 (tomatchl,tmsign)) - -let extract_arity_signatures env0 tomatchl tmsign = - let get_one_sign tm (na,t) = - match tm with - | NotInd (bo,typ) -> - (match t with - | None -> [na,bo,typ] - | Some (loc,_,_,_) -> - user_err_loc (loc,"", - str "Unexpected type annotation for a term of non inductive type")) - | IsInd (_,IndType(indf,realargs)) -> - let (ind,params) = dest_ind_family indf in - let nrealargs = List.length realargs in - let realnal = - match t with - | Some (loc,ind',nparams,realnal) -> - if ind <> ind' then - user_err_loc (loc,"",str "Wrong inductive type"); - if List.length params <> nparams - or nrealargs <> List.length realnal then - anomaly "Ill-formed 'in' clause in cases"; - List.rev realnal - | None -> list_tabulate (fun _ -> Anonymous) nrealargs in - let arsign = fst (get_arity env0 indf) in - (na,None,build_dependent_inductive env0 indf) - ::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign - with e when Errors.noncritical e -> assert false) in - let rec buildrec = function - | [],[] -> [] - | (_,tm)::ltm, x::tmsign -> - let l = get_one_sign tm x in - l :: buildrec (ltm,tmsign) - | _ -> assert false - in List.rev (buildrec (tomatchl,tmsign)) - -let inh_conv_coerce_to_tycon loc env isevars j tycon = - match tycon with - | Some p -> - let (evd',j) = Coercion.inh_conv_coerce_to true loc env !isevars j p in - isevars := evd'; - j - | None -> j - -let out_ind = function IsInd (_, IndType(x, y)) -> (x, y) | _ -> assert(false) - -let string_of_name name = - match name with - | Anonymous -> "anonymous" - | Name n -> string_of_id n - -let id_of_name n = id_of_string (string_of_name n) - -let make_prime_id name = - let str = string_of_name name in - id_of_string str, id_of_string (str ^ "'") - -let prime avoid name = - let previd, id = make_prime_id name in - previd, next_ident_away id avoid - -let make_prime avoid prevname = - let previd, id = prime !avoid prevname in - avoid := id :: !avoid; - previd, id - -let eq_id avoid id = - let hid = id_of_string ("Heq_" ^ string_of_id id) in - let hid' = next_ident_away hid avoid in - hid' - -let mk_eq typ x y = mkApp (delayed_force eq_ind, [| typ; x ; y |]) -let mk_eq_refl typ x = mkApp (delayed_force eq_refl, [| typ; x |]) -let mk_JMeq typ x typ' y = - mkApp (delayed_force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |]) -let mk_JMeq_refl typ x = mkApp (delayed_force Subtac_utils.jmeq_refl, [| typ; x |]) - -let hole = GHole (dummy_loc, Evd.QuestionMark (Evd.Define true)) - -let constr_of_pat env isevars arsign pat avoid = - let rec typ env (ty, realargs) pat avoid = - match pat with - | PatVar (l,name) -> - let name, avoid = match name with - Name n -> name, avoid - | Anonymous -> - let previd, id = prime avoid (Name (id_of_string "wildcard")) in - Name id, id :: avoid - in - PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid - | PatCstr (l,((_, i) as cstr),args,alias) -> - let cind = inductive_of_constructor cstr in - let IndType (indf, _) = - try find_rectype env ( !isevars) (lift (-(List.length realargs)) ty) - with Not_found -> error_case_not_inductive env - {uj_val = ty; uj_type = Typing.type_of env !isevars ty} - in - let ind, params = dest_ind_family indf in - if ind <> cind then error_bad_constructor_loc l cstr ind; - let cstrs = get_constructors env indf in - let ci = cstrs.(i-1) in - let nb_args_constr = ci.cs_nargs in - assert(nb_args_constr = List.length args); - let patargs, args, sign, env, n, m, avoid = - List.fold_right2 - (fun (na, c, t) ua (patargs, args, sign, env, n, m, avoid) -> - let pat', sign', arg', typ', argtypargs, n', avoid = - typ env (substl args (liftn (List.length sign) (succ (List.length args)) t), []) ua avoid - in - let args' = arg' :: List.map (lift n') args in - let env' = push_rels sign' env in - (pat' :: patargs, args', sign' @ sign, env', n' + n, succ m, avoid)) - ci.cs_args (List.rev args) ([], [], [], env, 0, 0, avoid) - in - let args = List.rev args in - let patargs = List.rev patargs in - let pat' = PatCstr (l, cstr, patargs, alias) in - let cstr = mkConstruct ci.cs_cstr in - let app = applistc cstr (List.map (lift (List.length sign)) params) in - let app = applistc app args in - let apptype = Retyping.get_type_of env ( !isevars) app in - let IndType (indf, realargs) = find_rectype env ( !isevars) apptype in - match alias with - Anonymous -> - pat', sign, app, apptype, realargs, n, avoid - | Name id -> - let sign = (alias, None, lift m ty) :: sign in - let avoid = id :: avoid in - let sign, i, avoid = - try - let env = push_rels sign env in - isevars := the_conv_x_leq (push_rels sign env) (lift (succ m) ty) (lift 1 apptype) !isevars; - let eq_t = mk_eq (lift (succ m) ty) - (mkRel 1) (* alias *) - (lift 1 app) (* aliased term *) - in - let neq = eq_id avoid id in - (Name neq, Some (mkRel 0), eq_t) :: sign, 2, neq :: avoid - with Reduction.NotConvertible -> sign, 1, avoid - in - (* Mark the equality as a hole *) - pat', sign, lift i app, lift i apptype, realargs, n + i, avoid - in - let pat', sign, patc, patty, args, z, avoid = typ env (pi3 (List.hd arsign), List.tl arsign) pat avoid in - pat', (sign, patc, (pi3 (List.hd arsign), args), pat'), avoid - - -(* shadows functional version *) -let eq_id avoid id = - let hid = id_of_string ("Heq_" ^ string_of_id id) in - let hid' = next_ident_away hid !avoid in - avoid := hid' :: !avoid; - hid' - -let rels_of_patsign = - List.map (fun ((na, b, t) as x) -> - match b with - | Some t' when kind_of_term t' = Rel 0 -> (na, None, t) - | _ -> x) - -let vars_of_ctx ctx = - let _, y = - List.fold_right (fun (na, b, t) (prev, vars) -> - match b with - | Some t' when kind_of_term t' = Rel 0 -> - prev, - (GApp (dummy_loc, - (GRef (dummy_loc, delayed_force refl_ref)), [hole; GVar (dummy_loc, prev)])) :: vars - | _ -> - match na with - Anonymous -> raise (Invalid_argument "vars_of_ctx") - | Name n -> n, GVar (dummy_loc, n) :: vars) - ctx (id_of_string "vars_of_ctx_error", []) - in List.rev y - -let rec is_included x y = - match x, y with - | PatVar _, _ -> true - | _, PatVar _ -> true - | PatCstr (l, (_, i), args, alias), PatCstr (l', (_, i'), args', alias') -> - if i = i' then List.for_all2 is_included args args' - else false - -(* liftsign is the current pattern's complete signature length. Hence pats is already typed in its - full signature. However prevpatterns are in the original one signature per pattern form. - *) -let build_ineqs prevpatterns pats liftsign = - let _tomatchs = List.length pats in - let diffs = - List.fold_left - (fun c eqnpats -> - let acc = List.fold_left2 - (* ppat is the pattern we are discriminating against, curpat is the current one. *) - (fun acc (ppat_sign, ppat_c, (ppat_ty, ppat_tyargs), ppat) - (curpat_sign, curpat_c, (curpat_ty, curpat_tyargs), curpat) -> - match acc with - None -> None - | Some (sign, len, n, c) -> (* FixMe: do not work with ppat_args *) - if is_included curpat ppat then - (* Length of previous pattern's signature *) - let lens = List.length ppat_sign in - (* Accumulated length of previous pattern's signatures *) - let len' = lens + len in - let acc = - ((* Jump over previous prevpat signs *) - lift_rel_context len ppat_sign @ sign, - len', - succ n, (* nth pattern *) - mkApp (delayed_force eq_ind, - [| lift (len' + liftsign) curpat_ty; - liftn (len + liftsign) (succ lens) ppat_c ; - lift len' curpat_c |]) :: - List.map (lift lens (* Jump over this prevpat signature *)) c) - in Some acc - else None) - (Some ([], 0, 0, [])) eqnpats pats - in match acc with - None -> c - | Some (sign, len, _, c') -> - let conj = it_mkProd_or_LetIn (mk_not (mk_conj c')) - (lift_rel_context liftsign sign) - in - conj :: c) - [] prevpatterns - in match diffs with [] -> None - | _ -> Some (mk_conj diffs) - -let subst_rel_context k ctx subst = - let (_, ctx') = - List.fold_right - (fun (n, b, t) (k, acc) -> - (succ k, (n, Option.map (substnl subst k) b, substnl subst k t) :: acc)) - ctx (k, []) - in ctx' - -let lift_rel_contextn n k sign = - let rec liftrec k = function - | (na,c,t)::sign -> - (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign) - | [] -> [] - in - liftrec (rel_context_length sign + k) sign - -let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity = - let i = ref 0 in - let (x, y, z) = - List.fold_left - (fun (branches, eqns, prevpatterns) eqn -> - let _, newpatterns, pats = - List.fold_left2 - (fun (idents, newpatterns, pats) pat arsign -> - let pat', cpat, idents = constr_of_pat env isevars arsign pat idents in - (idents, pat' :: newpatterns, cpat :: pats)) - ([], [], []) eqn.patterns sign - in - let newpatterns = List.rev newpatterns and opats = List.rev pats in - let rhs_rels, pats, signlen = - List.fold_left - (fun (renv, pats, n) (sign,c, (s, args), p) -> - (* Recombine signatures and terms of all of the row's patterns *) - let sign' = lift_rel_context n sign in - let len = List.length sign' in - (sign' @ renv, - (* lift to get outside of previous pattern's signatures. *) - (sign', liftn n (succ len) c, (s, List.map (liftn n (succ len)) args), p) :: pats, - len + n)) - ([], [], 0) opats in - let pats, _ = List.fold_left - (* lift to get outside of past patterns to get terms in the combined environment. *) - (fun (pats, n) (sign, c, (s, args), p) -> - let len = List.length sign in - ((rels_of_patsign sign, lift n c, (s, List.map (lift n) args), p) :: pats, len + n)) - ([], 0) pats - in - let ineqs = build_ineqs prevpatterns pats signlen in - let rhs_rels' = rels_of_patsign rhs_rels in - let _signenv = push_rel_context rhs_rels' env in - let arity = - let args, nargs = - List.fold_right (fun (sign, c, (_, args), _) (allargs,n) -> - (args @ c :: allargs, List.length args + succ n)) - pats ([], 0) - in - let args = List.rev args in - substl args (liftn signlen (succ nargs) arity) - in - let rhs_rels', tycon = - let neqs_rels, arity = - match ineqs with - | None -> [], arity - | Some ineqs -> - [Anonymous, None, ineqs], lift 1 arity - in - let eqs_rels, arity = decompose_prod_n_assum neqs arity in - eqs_rels @ neqs_rels @ rhs_rels', arity - in - let rhs_env = push_rels rhs_rels' env in - let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in - let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' - and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in - let branch_name = id_of_string ("program_branch_" ^ (string_of_int !i)) in - let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in - let branch = - let bref = GVar (dummy_loc, branch_name) in - match vars_of_ctx rhs_rels with - [] -> bref - | l -> GApp (dummy_loc, bref, l) - in - let branch = match ineqs with - Some _ -> GApp (dummy_loc, branch, [ hole ]) - | None -> branch - in - incr i; - let rhs = { eqn.rhs with it = branch } in - (branch_decl :: branches, - { eqn with patterns = newpatterns; rhs = rhs } :: eqns, - opats :: prevpatterns)) - ([], [], []) eqns - in x, y - -(* Builds the predicate. If the predicate is dependent, its context is - * made of 1+nrealargs assumptions for each matched term in an inductive - * type and 1 assumption for each term not _syntactically_ in an - * inductive type. - - * Each matched terms are independently considered dependent or not. - - * A type constraint but no annotation case: it is assumed non dependent. - *) - -let lift_ctx n ctx = - let ctx', _ = - List.fold_right (fun (c, t) (ctx, n') -> (liftn n n' c, liftn_tomatch_type n n' t) :: ctx, succ n') ctx ([], 0) - in ctx' - -(* Turn matched terms into variables. *) -let abstract_tomatch env tomatchs tycon = - let prev, ctx, names, tycon = - List.fold_left - (fun (prev, ctx, names, tycon) (c, t) -> - let lenctx = List.length ctx in - match kind_of_term c with - Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names, tycon - | _ -> - let tycon = Option.map - (fun t -> subst_term (lift 1 c) (lift 1 t)) tycon in - let name = next_ident_away (id_of_string "filtered_var") names in - (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev, - (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx, - name :: names, tycon) - ([], [], [], tycon) tomatchs - in List.rev prev, ctx, tycon - -let is_dependent_ind = function - IsInd (_, IndType (indf, args)) when List.length args > 0 -> true - | _ -> false - -let build_dependent_signature env evars avoid tomatchs arsign = - let avoid = ref avoid in - let arsign = List.rev arsign in - let allnames = List.rev (List.map (List.map pi1) arsign) in - let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in - let eqs, neqs, refls, slift, arsign' = - List.fold_left2 - (fun (eqs, neqs, refl_args, slift, arsigns) (tm, ty) arsign -> - (* The accumulator: - previous eqs, - number of previous eqs, - lift to get outside eqs and in the introduced variables ('as' and 'in'), - new arity signatures - *) - match ty with - IsInd (ty, IndType (indf, args)) when List.length args > 0 -> - (* Build the arity signature following the names in matched terms as much as possible *) - let argsign = List.tl arsign in (* arguments in inverse application order *) - let (appn, appb, appt) as _appsign = List.hd arsign in (* The matched argument *) - let argsign = List.rev argsign in (* arguments in application order *) - let env', nargeqs, argeqs, refl_args, slift, argsign' = - List.fold_left2 - (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg (name, b, t) -> - let argt = Retyping.get_type_of env evars arg in - let eq, refl_arg = - if Reductionops.is_conv env evars argt t then - (mk_eq (lift (nargeqs + slift) argt) - (mkRel (nargeqs + slift)) - (lift (nargeqs + nar) arg), - mk_eq_refl argt arg) - else - (mk_JMeq (lift (nargeqs + slift) t) - (mkRel (nargeqs + slift)) - (lift (nargeqs + nar) argt) - (lift (nargeqs + nar) arg), - mk_JMeq_refl argt arg) - in - let previd, id = - let name = - match kind_of_term arg with - Rel n -> pi1 (lookup_rel n env) - | _ -> name - in - make_prime avoid name - in - (env, succ nargeqs, - (Name (eq_id avoid previd), None, eq) :: argeqs, - refl_arg :: refl_args, - pred slift, - (Name id, b, t) :: argsign')) - (env, neqs, [], [], slift, []) args argsign - in - let eq = mk_JMeq - (lift (nargeqs + slift) appt) - (mkRel (nargeqs + slift)) - (lift (nargeqs + nar) ty) - (lift (nargeqs + nar) tm) - in - let refl_eq = mk_JMeq_refl ty tm in - let previd, id = make_prime avoid appn in - (((Name (eq_id avoid previd), None, eq) :: argeqs) :: eqs, - succ nargeqs, - refl_eq :: refl_args, - pred slift, - (((Name id, appb, appt) :: argsign') :: arsigns)) - - | _ -> - (* Non dependent inductive or not inductive, just use a regular equality *) - let (name, b, typ) = match arsign with [x] -> x | _ -> assert(false) in - let previd, id = make_prime avoid name in - let arsign' = (Name id, b, typ) in - let tomatch_ty = type_of_tomatch ty in - let eq = - mk_eq (lift nar tomatch_ty) - (mkRel slift) (lift nar tm) - in - ([(Name (eq_id avoid previd), None, eq)] :: eqs, succ neqs, - (mk_eq_refl tomatch_ty tm) :: refl_args, - pred slift, (arsign' :: []) :: arsigns)) - ([], 0, [], nar, []) tomatchs arsign - in - let arsign'' = List.rev arsign' in - assert(slift = 0); (* we must have folded over all elements of the arity signature *) - arsign'', allnames, nar, eqs, neqs, refls - -(**************************************************************************) -(* Main entry of the matching compilation *) - -let liftn_rel_context n k sign = - let rec liftrec k = function - | (na,c,t)::sign -> - (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign) - | [] -> [] - in - liftrec (k + rel_context_length sign) sign - -let nf_evars_env sigma (env : env) : env = - let nf t = nf_evar sigma t in - let env0 : env = reset_context env in - let f e (na, b, t) e' : env = - Environ.push_named (na, Option.map nf b, nf t) e' - in - let env' = Environ.fold_named_context f ~init:env0 env in - Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, Option.map nf b, nf t) e') - ~init:env' env - - -let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp = - (* We extract the signature of the arity *) - let arsign = extract_arity_signature env tomatchs sign in - let newenv = List.fold_right push_rels arsign env in - let allnames = List.rev (List.map (List.map pi1) arsign) in - match rtntyp with - | Some rtntyp -> - let predcclj = typing_fun (mk_tycon (new_Type ())) newenv rtntyp in - let predccl = (j_nf_evar !isevars predcclj).uj_val in - Some (build_initial_predicate true allnames predccl) - | None -> - match valcon_of_tycon tycon with - | Some ty -> - let pred = - prepare_predicate_from_arsign_tycon loc env !isevars tomatchs arsign ty - in Some (build_initial_predicate true allnames pred) - | None -> None - -let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) = - - let typing_fun tycon env = typing_fun tycon env isevars in - - (* We build the matrix of patterns and right-hand side *) - let matx = matx_of_eqns env eqns in - - (* We build the vector of terms to match consistently with the *) - (* constructors found in patterns *) - let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in - let _isdep = List.exists (fun (x, y) -> is_dependent_ind y) tomatchs in - if predopt = None then - let tycon = valcon_of_tycon tycon in - let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env tomatchs tycon in - let env = push_rel_context tomatchs_lets env in - let len = List.length eqns in - let sign, allnames, signlen, eqs, neqs, args = - (* The arity signature *) - let arsign = extract_arity_signatures env tomatchs (List.map snd tomatchl) in - (* Build the dependent arity signature, the equalities which makes - the first part of the predicate and their instantiations. *) - let avoid = [] in - build_dependent_signature env ( !isevars) avoid tomatchs arsign - - in - let tycon, arity = - match tycon' with - | None -> let ev = mkExistential env isevars in ev, ev - | Some t -> - Option.get tycon, prepare_predicate_from_arsign_tycon loc env ( !isevars) - tomatchs sign t - in - let neqs, arity = - let ctx = context_of_arsign eqs in - let neqs = List.length ctx in - neqs, it_mkProd_or_LetIn (lift neqs arity) ctx - in - let lets, matx = - (* Type the rhs under the assumption of equations *) - constrs_of_pats typing_fun env isevars matx tomatchs sign neqs arity - in - let matx = List.rev matx in - let _ = assert(len = List.length lets) in - let env = push_rels lets env in - let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in - let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in - let args = List.rev_map (lift len) args in - let pred = liftn len (succ signlen) arity in - let pred = build_initial_predicate true allnames pred in - - (* We push the initial terms to match and push their alias to rhs' envs *) - (* names of aliases will be recovered from patterns (hence Anonymous here) *) - let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in - - let pb = - { env = env; - isevars = isevars; - pred = Some pred; - tomatch = initial_pushed; - history = start_history (List.length initial_pushed); - mat = matx; - caseloc = loc; - casestyle= style; - typing_function = typing_fun } in - - let j = compile pb in - (* We check for unused patterns *) - List.iter (check_unused_pattern env) matx; - let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in - let j = - { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; - uj_type = nf_evar !isevars tycon; } - in j - else - (* We build the elimination predicate if any and check its consistency *) - (* with the type of arguments to match *) - let tmsign = List.map snd tomatchl in - let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon predopt in - - (* We push the initial terms to match and push their alias to rhs' envs *) - (* names of aliases will be recovered from patterns (hence Anonymous here) *) - let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in - let pb = - { env = env; - isevars = isevars; - pred = pred; - tomatch = initial_pushed; - history = start_history (List.length initial_pushed); - mat = matx; - caseloc = loc; - casestyle= style; - typing_function = typing_fun } in - - let j = compile pb in - (* We check for unused patterns *) - List.iter (check_unused_pattern env) matx; - inh_conv_coerce_to_tycon loc env isevars j tycon - -end - diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli deleted file mode 100644 index 5ef42b13..00000000 --- a/plugins/subtac/subtac_cases.mli +++ /dev/null @@ -1,21 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i*) -open Util -open Names -open Term -open Evd -open Environ -open Inductiveops -open Glob_term -open Evarutil -(*i*) - -(*s Compilation of pattern-matching, subtac style. *) -module Cases_F(C : Coercion.S) : Cases.S diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml deleted file mode 100644 index b0054d82..00000000 --- a/plugins/subtac/subtac_classes.ml +++ /dev/null @@ -1,190 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Pretyping -open Evd -open Environ -open Term -open Glob_term -open Topconstr -open Names -open Libnames -open Pp -open Vernacexpr -open Constrintern -open Subtac_command -open Typeclasses -open Typeclasses_errors -open Decl_kinds -open Entries -open Util - -module SPretyping = Subtac_pretyping.Pretyping - -let interp_constr_evars_gen evdref env ?(impls=Constrintern.empty_internalization_env) kind c = - SPretyping.understand_tcc_evars evdref env kind - (intern_gen (kind=IsType) ~impls !evdref env c) - -let interp_casted_constr_evars evdref env ?(impls=Constrintern.empty_internalization_env) c typ = - interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c - -let interp_context_evars evdref env params = - let impls_env, bl = Constrintern.interp_context_gen - (fun env t -> SPretyping.understand_tcc_evars evdref env IsType t) - (SPretyping.understand_judgment_tcc evdref) !evdref env params in bl - -let interp_type_evars_impls ~evdref ?(impls=empty_internalization_env) env c = - let c = intern_gen true ~impls !evdref env c in - let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in - SPretyping.understand_tcc_evars ~fail_evar:false evdref env IsType c, imps - -let type_ctx_instance evars env ctx inst subst = - let rec aux (subst, instctx) l = function - (na, b, t) :: ctx -> - let t' = substl subst t in - let c', l = - match b with - | None -> interp_casted_constr_evars evars env (List.hd l) t', List.tl l - | Some b -> substl subst b, l - in - evars := resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~fail:true env !evars; - let d = na, Some c', t' in - aux (c' :: subst, d :: instctx) l ctx - | [] -> subst - in aux (subst, []) inst (List.rev ctx) - -let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) pri = - let env = Global.env() in - let evars = ref Evd.empty in - let tclass, _ = - match bk with - | Implicit -> - Implicit_quantifiers.implicit_application Idset.empty (* need no avoid *) - ~allow_partial:false (fun avoid (clname, (id, _, t)) -> - match clname with - | Some (cl, b) -> - let t = - if b then - let _k = class_info cl in - CHole (Util.dummy_loc, Some Evd.InternalHole) - else CHole (Util.dummy_loc, None) - in t, avoid - | None -> failwith ("new instance: under-applied typeclass")) - cl - | Explicit -> cl, Idset.empty - in - let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in - let k, cty, ctx', ctx, len, imps, subst = - let (env', ctx), imps = interp_context_evars evars env ctx in - let c', imps' = interp_type_evars_impls ~evdref:evars env' tclass 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 cl, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in - let _, args = - List.fold_right (fun (na, b, t) (args, args') -> - match b with - | None -> (List.tl args, List.hd args :: args') - | Some b -> (args, substl args' b :: args')) - (snd cl.cl_context) (args, []) - in - cl, c', ctx', ctx, len, imps, args - in - let id = - match snd instid with - | Name id -> - let sp = Lib.make_path id in - if Nametab.exists_cci sp then - errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists"); - id - | Anonymous -> - let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in - Namegen.next_global_ident_away i (Termops.ids_of_context env) - in - evars := resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~fail:true env !evars; - let ctx = Evarutil.nf_rel_context_evar !evars ctx - and ctx' = Evarutil.nf_rel_context_evar !evars ctx' in - let env' = push_rel_context ctx env in - let sigma = !evars in - let subst = List.map (Evarutil.nf_evar sigma) subst in - let props = - match props with - | Some (CRecord (loc, _, fs)) -> - if List.length fs > List.length k.cl_props then - Classes.mismatched_props env' (List.map snd fs) k.cl_props; - Inl fs - | Some p -> Inr p - | None -> Inl [] - in - let subst = - match props with - | Inr term -> - let c = interp_casted_constr_evars evars env' term cty in - Inr c - | Inl props -> - let get_id = - function - | Ident id' -> id' - | _ -> errorlabstrm "new_instance" (Pp.str "Only local structures are handled") - in - let props, rest = - List.fold_left - (fun (props, rest) (id,b,_) -> - if b = None then - try - let (loc_mid, c) = List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest in - let rest' = List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest in - let (loc, mid) = get_id loc_mid in - List.iter - (fun (n, _, x) -> - if 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 (Util.dummy_loc, None) :: props), rest - else props, rest) - ([], props) k.cl_props - in - if rest <> [] then - unbound_method env' k.cl_impl (get_id (fst (List.hd rest))) - else - Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst) - in - evars := Evarutil.nf_evar_map !evars; - evars := resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~fail:true env !evars; - evars := resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:false env !evars; - let term, termtype = - match subst with - | Inl subst -> - let subst = List.fold_left2 - (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst') - [] subst (k.cl_props @ snd k.cl_context) - in - let app, ty_constr = instance_constructor k 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 - term, termtype - | Inr def -> - let termtype = it_mkProd_or_LetIn cty ctx in - let term = Termops.it_mkLambda_or_LetIn def ctx in - term, termtype - in - let termtype = Evarutil.nf_evar !evars termtype in - let term = Evarutil.nf_evar !evars term in - evars := undefined_evars !evars; - Evarutil.check_evars env Evd.empty !evars termtype; - 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 pri (not global) (ConstRef cst) - in - let evm = Subtac_utils.evars_of_term !evars Evd.empty term in - let obls, _, constr, typ = Eterm.eterm_obligations env id !evars evm 0 term termtype in - id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,Instance) ~hook obls diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli deleted file mode 100644 index bd3fe484..00000000 --- a/plugins/subtac/subtac_classes.mli +++ /dev/null @@ -1,39 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i*) -open Names -open Decl_kinds -open Term -open Sign -open Evd -open Environ -open Nametab -open Mod_subst -open Topconstr -open Util -open Typeclasses -open Implicit_quantifiers -open Classes -(*i*) - -val type_ctx_instance : Evd.evar_map ref -> - Environ.env -> - ('a * Term.constr option * Term.constr) list -> - Topconstr.constr_expr list -> - Term.constr list -> - Term.constr list - -val new_instance : - ?global:bool -> - local_binder list -> - typeclass_constraint -> - constr_expr option -> - ?generalize:bool -> - int option -> - identifier * Subtac_obligations.progress diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml deleted file mode 100644 index 4fe29ac8..00000000 --- a/plugins/subtac/subtac_coercion.ml +++ /dev/null @@ -1,510 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -open Util -open Names -open Term -open Reductionops -open Environ -open Typeops -open Pretype_errors -open Classops -open Recordops -open Evarutil -open Evarconv -open Retyping -open Evd - -open Global -open Subtac_utils -open Coqlib -open Printer -open Subtac_errors -open Eterm -open Pp - -let app_opt env evars f t = - whd_betaiota !evars (app_opt f t) - -let pair_of_array a = (a.(0), a.(1)) -let make_name s = Name (id_of_string s) - -let rec disc_subset x = - match kind_of_term x with - | App (c, l) -> - (match kind_of_term c with - Ind i -> - let len = Array.length l in - let sig_ = delayed_force sig_ in - if len = 2 && i = Term.destInd sig_.typ - then - let (a, b) = pair_of_array l in - Some (a, b) - else None - | _ -> None) - | _ -> None - -and disc_exist env x = - match kind_of_term x with - | App (c, l) -> - (match kind_of_term c with - Construct c -> - if c = Term.destConstruct (delayed_force sig_).intro - then Some (l.(0), l.(1), l.(2), l.(3)) - else None - | _ -> None) - | _ -> None - -module Coercion = struct - - exception NoSubtacCoercion - - let disc_proj_exist env x = - match kind_of_term x with - | App (c, l) -> - (if Term.eq_constr c (delayed_force sig_).proj1 - && Array.length l = 3 - then disc_exist env l.(2) - else None) - | _ -> None - - - let sort_rel s1 s2 = - match s1, s2 with - Prop Pos, Prop Pos -> Prop Pos - | Prop Pos, Prop Null -> Prop Null - | Prop Null, Prop Null -> Prop Null - | Prop Null, Prop Pos -> Prop Pos - | Type _, Prop Pos -> Prop Pos - | Type _, Prop Null -> Prop Null - | _, Type _ -> s2 - - let hnf env isevars c = whd_betadeltaiota env isevars c - let hnf_nodelta env evars c = whd_betaiota evars c - - let lift_args n sign = - let rec liftrec k = function - | t::sign -> liftn n k t :: (liftrec (k-1) sign) - | [] -> [] - in - liftrec (List.length sign) sign - - let rec mu env isevars t = - let rec aux v = - let v = hnf env !isevars v in - match disc_subset v with - Some (u, p) -> - let f, ct = aux u in - let p = hnf env !isevars p in - (Some (fun x -> - app_opt env isevars - f (mkApp ((delayed_force sig_).proj1, - [| u; p; x |]))), - ct) - | None -> (None, v) - in aux t - - and coerce loc env isevars (x : Term.constr) (y : Term.constr) - : (Term.constr -> Term.constr) option - = - let rec coerce_unify env x y = - let x = hnf env !isevars x and y = hnf env !isevars y in - try - isevars := the_conv_x_leq env x y !isevars; - None - with Reduction.NotConvertible -> coerce' env x y - and coerce' env x y : (Term.constr -> Term.constr) option = - let subco () = subset_coerce env isevars x y in - let dest_prod c = - match Reductionops.splay_prod_n env ( !isevars) 1 c with - | [(na,b,t)], c -> (na,t), c - | _ -> raise NoSubtacCoercion - in - let rec coerce_application typ typ' c c' l l' = - let len = Array.length l in - let rec aux tele typ typ' i co = - if i < len then - let hdx = l.(i) and hdy = l'.(i) in - try isevars := the_conv_x_leq env hdx hdy !isevars; - let (n, eqT), restT = dest_prod typ in - let (n', eqT'), restT' = dest_prod typ' in - aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co - with Reduction.NotConvertible -> - let (n, eqT), restT = dest_prod typ in - let (n', eqT'), restT' = dest_prod typ' in - let _ = - try isevars := the_conv_x_leq env eqT eqT' !isevars - with Reduction.NotConvertible -> raise NoSubtacCoercion - in - (* Disallow equalities on arities *) - if Reduction.is_arity env eqT then raise NoSubtacCoercion; - let restargs = lift_args 1 - (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i))))) - in - let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in - let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in - let eq = mkApp (delayed_force eq_ind, [| eqT; hdx; hdy |]) in - let evar = make_existential loc env isevars eq in - let eq_app x = mkApp (delayed_force eq_rect, - [| eqT; hdx; pred; x; hdy; evar|]) in - aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) - else Some co - in - if isEvar c || isEvar c' then - (* Second-order unification needed. *) - raise NoSubtacCoercion; - aux [] typ typ' 0 (fun x -> x) - in - match (kind_of_term x, kind_of_term y) with - | Sort s, Sort s' -> - (match s, s' with - Prop x, Prop y when x = y -> None - | Prop _, Type _ -> None - | Type x, Type y when x = y -> None (* false *) - | _ -> subco ()) - | Prod (name, a, b), Prod (name', a', b') -> - let name' = Name (Namegen.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in - let env' = push_rel (name', None, a') env in - let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in - (* env, x : a' |- c1 : lift 1 a' > lift 1 a *) - let coec1 = app_opt env' isevars c1 (mkRel 1) in - (* env, x : a' |- c1[x] : lift 1 a *) - let c2 = coerce_unify env' (subst1 coec1 (liftn 1 2 b)) b' in - (* env, x : a' |- c2 : b[c1[x]/x]] > b' *) - (match c1, c2 with - | None, None -> None - | _, _ -> - Some - (fun f -> - mkLambda (name', a', - app_opt env' isevars c2 - (mkApp (Term.lift 1 f, [| coec1 |]))))) - - | App (c, l), App (c', l') -> - (match kind_of_term c, kind_of_term c' with - Ind i, Ind i' -> (* Inductive types *) - let len = Array.length l in - let existS = delayed_force existS in - let prod = delayed_force prod in - (* Sigma types *) - if len = Array.length l' && len = 2 && i = i' - && (i = Term.destInd existS.typ || i = Term.destInd prod.typ) - then - if i = Term.destInd existS.typ - then - begin - let (a, pb), (a', pb') = - pair_of_array l, pair_of_array l' - in - let c1 = coerce_unify env a a' in - let rec remove_head a c = - match kind_of_term c with - | Lambda (n, t, t') -> c, t' - (*| Prod (n, t, t') -> t'*) - | Evar (k, args) -> - let (evs, t) = Evarutil.define_evar_as_lambda env !isevars (k,args) in - isevars := evs; - let (n, dom, rng) = destLambda t in - let (domk, args) = destEvar dom in - isevars := define domk a !isevars; - t, rng - | _ -> raise NoSubtacCoercion - in - let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in - let env' = push_rel (make_name "x", None, a) env in - let c2 = coerce_unify env' b b' in - match c1, c2 with - None, None -> - None - | _, _ -> - Some - (fun x -> - let x, y = - app_opt env' isevars c1 (mkApp (existS.proj1, - [| a; pb; x |])), - app_opt env' isevars c2 (mkApp (existS.proj2, - [| a; pb; x |])) - in - mkApp (existS.intro, [| a'; pb'; x ; y |])) - end - else - begin - let (a, b), (a', b') = - pair_of_array l, pair_of_array l' - in - let c1 = coerce_unify env a a' in - let c2 = coerce_unify env b b' in - match c1, c2 with - None, None -> None - | _, _ -> - Some - (fun x -> - let x, y = - app_opt env isevars c1 (mkApp (prod.proj1, - [| a; b; x |])), - app_opt env isevars c2 (mkApp (prod.proj2, - [| a; b; x |])) - in - mkApp (prod.intro, [| a'; b'; x ; y |])) - end - else - if i = i' && len = Array.length l' then - let evm = !isevars in - (try subco () - with NoSubtacCoercion -> - let typ = Typing.type_of env evm c in - let typ' = Typing.type_of env evm c' in - (* if not (is_arity env evm typ) then *) - coerce_application typ typ' c c' l l') - (* else subco () *) - else - subco () - | x, y when x = y -> - if Array.length l = Array.length l' then - let evm = !isevars in - let lam_type = Typing.type_of env evm c in - let lam_type' = Typing.type_of env evm c' in -(* if not (is_arity env evm lam_type) then ( *) - coerce_application lam_type lam_type' c c' l l' -(* ) else subco () *) - else subco () - | _ -> subco ()) - | _, _ -> subco () - - and subset_coerce env isevars x y = - match disc_subset x with - Some (u, p) -> - let c = coerce_unify env u y in - let f x = - app_opt env isevars c (mkApp ((delayed_force sig_).proj1, - [| u; p; x |])) - in Some f - | None -> - match disc_subset y with - Some (u, p) -> - let c = coerce_unify env x u in - Some - (fun x -> - let cx = app_opt env isevars c x in - let evar = make_existential loc env isevars (mkApp (p, [| cx |])) - in - (mkApp - ((delayed_force sig_).intro, - [| u; p; cx; evar |]))) - | None -> - raise NoSubtacCoercion - (*isevars := Evd.add_conv_pb (Reduction.CONV, x, y) !isevars; - None*) - in coerce_unify env x y - - let coerce_itf loc env isevars v t c1 = - let evars = ref isevars in - let coercion = coerce loc env evars t c1 in - let t = Option.map (app_opt env evars coercion) v in - !evars, t - - (* Taken from pretyping/coercion.ml *) - - (* Typing operations dealing with coercions *) - - (* Here, funj is a coercion therefore already typed in global context *) - let apply_coercion_args env argl funj = - let rec apply_rec acc typ = function - | [] -> { uj_val = applist (j_val funj,argl); - uj_type = typ } - | h::restl -> - (* On devrait pouvoir s'arranger pour qu'on n'ait pas Ć faire hnf_constr *) - match kind_of_term (whd_betadeltaiota env Evd.empty typ) with - | Prod (_,c1,c2) -> - (* Typage garanti par l'appel Ć app_coercion*) - apply_rec (h::acc) (subst1 h c2) restl - | _ -> anomaly "apply_coercion_args" - in - apply_rec [] funj.uj_type argl - - (* appliquer le chemin de coercions de patterns p *) - exception NoCoercion - - let apply_pattern_coercion loc pat p = - List.fold_left - (fun pat (co,n) -> - let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in - Glob_term.PatCstr (loc, co, list_tabulate f (n+1), Anonymous)) - pat p - - (* raise Not_found if no coercion found *) - let inh_pattern_coerce_to loc pat ind1 ind2 = - let p = lookup_pattern_path_between (ind1,ind2) in - apply_pattern_coercion loc pat p - - (* appliquer le chemin de coercions p Ć hj *) - - let apply_coercion env sigma p hj typ_cl = - try - fst (List.fold_left - (fun (ja,typ_cl) i -> - let fv,isid = coercion_value i in - let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in - let jres = apply_coercion_args env argl fv in - (if isid then - { uj_val = ja.uj_val; uj_type = jres.uj_type } - else - jres), - jres.uj_type) - (hj,typ_cl) p) - with e when Errors.noncritical e -> anomaly "apply_coercion" - - let inh_app_fun _ env isevars j = - let isevars = ref isevars in - let t = hnf env !isevars j.uj_type in - match kind_of_term t with - | Prod (_,_,_) -> (!isevars,j) - | Evar ev when not (is_defined_evar !isevars ev) -> - let (isevars',t) = define_evar_as_product !isevars ev in - (isevars',{ uj_val = j.uj_val; uj_type = t }) - | _ -> - (try - let t,p = - lookup_path_to_fun_from env !isevars j.uj_type in - (!isevars,apply_coercion env !isevars p j t) - with Not_found -> - try - let coercef, t = mu env isevars t in - let res = { uj_val = app_opt env isevars coercef j.uj_val; uj_type = t } in - (!isevars, res) - with NoSubtacCoercion | NoCoercion -> - (!isevars,j)) - - let inh_tosort_force loc env isevars j = - try - let t,p = lookup_path_to_sort_from env ( isevars) j.uj_type in - let j1 = apply_coercion env ( isevars) p j t in - (isevars, type_judgment env (j_nf_evar ( isevars) j1)) - with Not_found -> - error_not_a_type_loc loc env ( isevars) j - - let inh_coerce_to_sort loc env isevars j = - let typ = hnf env isevars j.uj_type in - match kind_of_term typ with - | Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s }) - | Evar ev when not (is_defined_evar isevars ev) -> - let (isevars',s) = define_evar_as_sort isevars ev in - (isevars',{ utj_val = j.uj_val; utj_type = s }) - | _ -> - inh_tosort_force loc env isevars j - - let inh_coerce_to_base loc env isevars j = - let isevars = ref isevars in - let typ = hnf env !isevars j.uj_type in - let ct, typ' = mu env isevars typ in - let res = - { uj_val = app_opt env isevars ct j.uj_val; - uj_type = typ' } - in !isevars, res - - let inh_coerce_to_prod loc env isevars t = - let isevars = ref isevars in - let typ = hnf env !isevars (snd t) in - let _, typ' = mu env isevars typ in - !isevars, (fst t, typ') - - let inh_coerce_to_fail env evd rigidonly v t c1 = - if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t) - then - raise NoCoercion - else - let v', t' = - try - let t2,t1,p = lookup_path_between env evd (t,c1) in - match v with - Some v -> - let j = apply_coercion env evd p - {uj_val = v; uj_type = t} t2 in - Some j.uj_val, j.uj_type - | None -> None, t - with Not_found -> raise NoCoercion - in - try (the_conv_x_leq env t' c1 evd, v') - with Reduction.NotConvertible -> raise NoCoercion - - - let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = - try (the_conv_x_leq env t c1 evd, v) - with Reduction.NotConvertible -> - try inh_coerce_to_fail env evd rigidonly v t c1 - with NoCoercion -> - match - kind_of_term (whd_betadeltaiota env evd t), - kind_of_term (whd_betadeltaiota env evd c1) - with - | Prod (name,t1,t2), Prod (_,u1,u2) -> - (* Conversion did not work, we may succeed with a coercion. *) - (* We eta-expand (hence possibly modifying the original term!) *) - (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *) - (* has type forall (x:u1), u2 (with v' recursively obtained) *) - let name = match name with - | Anonymous -> Name (id_of_string "x") - | _ -> name in - let env1 = push_rel (name,None,u1) env in - let (evd', v1) = - inh_conv_coerce_to_fail loc env1 evd rigidonly - (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in - let v1 = Option.get v1 in - let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in - let t2 = Termops.subst_term v1 t2 in - let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in - (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') - | _ -> raise NoCoercion - - (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) - let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) = - match n with - | None -> - let cj = { cj with uj_type = hnf_nodelta env evd cj.uj_type } - and t = hnf_nodelta env evd t in - let (evd', val') = - try - inh_conv_coerce_to_fail loc env evd rigidonly - (Some cj.uj_val) cj.uj_type t - with NoCoercion -> - (try - coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t - with NoSubtacCoercion -> - error_actual_type_loc loc env evd cj t) - in - let val' = match val' with Some v -> v | None -> assert(false) in - (evd',{ uj_val = val'; uj_type = t }) - | Some (init, cur) -> - (evd, cj) - - let inh_conv_coerce_to _ = inh_conv_coerce_to_gen false - let inh_conv_coerce_rigid_to _ = inh_conv_coerce_to_gen true - - let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) = - let nabsinit, nabs = - match abs with - None -> 0, 0 - | Some (init, cur) -> init, cur - in - try - let rels, rng = Reductionops.splay_prod_n env ( isevars) nabs t in - (* The final range free variables must have been replaced by evars, we accept only that evars - in rng are applied to free vars. *) - if noccur_with_meta 1 (succ nabs) rng then ( - let env', t, t' = - let env' = push_rel_context rels env in - env', rng, lift nabs t' - in - try - fst (try inh_conv_coerce_to_fail loc env' isevars false None t t' - with NoCoercion -> - coerce_itf loc env' isevars None t t') - with NoSubtacCoercion -> - error_cannot_coerce env' isevars (t, t')) - else isevars - with e when Errors.noncritical e -> isevars -end diff --git a/plugins/subtac/subtac_coercion.mli b/plugins/subtac/subtac_coercion.mli deleted file mode 100644 index 5678c10e..00000000 --- a/plugins/subtac/subtac_coercion.mli +++ /dev/null @@ -1,4 +0,0 @@ -open Term -val disc_subset : types -> (types * types) option - -module Coercion : Coercion.S 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 diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli deleted file mode 100644 index 72549a01..00000000 --- a/plugins/subtac/subtac_command.mli +++ /dev/null @@ -1,60 +0,0 @@ -open Pretyping -open Evd -open Environ -open Term -open Topconstr -open Names -open Libnames -open Pp -open Vernacexpr -open Constrintern - -val interp_gen : - typing_constraint -> - evar_map ref -> - env -> - ?impls:internalization_env -> - ?allow_patvar:bool -> - ?ltacvars:ltac_sign -> - constr_expr -> constr -val interp_constr : - evar_map ref -> - env -> constr_expr -> constr -val interp_type_evars : - evar_map ref -> - env -> - ?impls:internalization_env -> - constr_expr -> constr -val interp_casted_constr_evars : - evar_map ref -> - env -> - ?impls:internalization_env -> - constr_expr -> types -> constr -val interp_open_constr : - evar_map ref -> env -> constr_expr -> constr -val interp_constr_judgment : - evar_map ref -> - env -> - constr_expr -> unsafe_judgment -val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list - -val interp_binder : Evd.evar_map ref -> - Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr - - -val telescope : - (Names.name * Term.types option * Term.types) list -> - Term.types * (Names.name * Term.types option * Term.types) list * - Term.constr - -val build_wellfounded : - Names.identifier * 'a * Topconstr.local_binder list * - Topconstr.constr_expr * Topconstr.constr_expr -> - Topconstr.constr_expr -> - Topconstr.constr_expr -> 'b -> Subtac_obligations.progress - -val build_recursive : - (fixpoint_expr * decl_notation list) list -> unit - -val build_corecursive : - (cofixpoint_expr * decl_notation list) list -> unit diff --git a/plugins/subtac/subtac_errors.ml b/plugins/subtac/subtac_errors.ml deleted file mode 100644 index 067da150..00000000 --- a/plugins/subtac/subtac_errors.ml +++ /dev/null @@ -1,24 +0,0 @@ -open Util -open Pp -open Printer - -type term_pp = Pp.std_ppcmds - -type subtyping_error = - | UncoercibleInferType of loc * term_pp * term_pp - | UncoercibleInferTerm of loc * term_pp * term_pp * term_pp * term_pp - | UncoercibleRewrite of term_pp * term_pp - -type typing_error = - | NonFunctionalApp of loc * term_pp * term_pp * term_pp - | NonConvertible of loc * term_pp * term_pp - | NonSigma of loc * term_pp - | IllSorted of loc * term_pp - -exception Subtyping_error of subtyping_error -exception Typing_error of typing_error - -exception Debug_msg of string - -let typing_error e = raise (Typing_error e) -let subtyping_error e = raise (Subtyping_error e) diff --git a/plugins/subtac/subtac_errors.mli b/plugins/subtac/subtac_errors.mli deleted file mode 100644 index 8d75b9c0..00000000 --- a/plugins/subtac/subtac_errors.mli +++ /dev/null @@ -1,15 +0,0 @@ -type term_pp = Pp.std_ppcmds -type subtyping_error = - UncoercibleInferType of Util.loc * term_pp * term_pp - | UncoercibleInferTerm of Util.loc * term_pp * term_pp * term_pp * term_pp - | UncoercibleRewrite of term_pp * term_pp -type typing_error = - NonFunctionalApp of Util.loc * term_pp * term_pp * term_pp - | NonConvertible of Util.loc * term_pp * term_pp - | NonSigma of Util.loc * term_pp - | IllSorted of Util.loc * term_pp -exception Subtyping_error of subtyping_error -exception Typing_error of typing_error -exception Debug_msg of string -val typing_error : typing_error -> 'a -val subtyping_error : subtyping_error -> 'a diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml deleted file mode 100644 index 7a4916fa..00000000 --- a/plugins/subtac/subtac_obligations.ml +++ /dev/null @@ -1,699 +0,0 @@ -open Printf -open Pp -open Subtac_utils -open Command -open Environ - -open Term -open Names -open Libnames -open Summary -open Libobject -open Entries -open Decl_kinds -open Util -open Evd -open Declare -open Proof_type -open Compat - -let ppwarn cmd = Pp.warn (str"Program:" ++ cmd) -let pperror cmd = Util.errorlabstrm "Program" cmd -let error s = pperror (str s) - -let reduce c = - Reductionops.clos_norm_flags Closure.betaiota (Global.env ()) Evd.empty c - -exception NoObligations of identifier option - -let explain_no_obligations = function - Some ident -> str "No obligations for program " ++ str (string_of_id ident) - | None -> str "No obligations remaining" - -type obligation_info = (Names.identifier * Term.types * hole_kind located * - obligation_definition_status * Intset.t * tactic option) array - -type obligation = - { obl_name : identifier; - obl_type : types; - obl_location : hole_kind located; - obl_body : constr option; - obl_status : obligation_definition_status; - obl_deps : Intset.t; - obl_tac : tactic option; - } - -type obligations = (obligation array * int) - -type fixpoint_kind = - | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list - | IsCoFixpoint - -type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list - -type program_info = { - prg_name: identifier; - prg_body: constr; - prg_type: constr; - prg_obligations: obligations; - prg_deps : identifier list; - prg_fixkind : fixpoint_kind option ; - prg_implicits : (Topconstr.explicitation * (bool * bool * bool)) list; - prg_notations : notations ; - prg_kind : definition_kind; - prg_reduce : constr -> constr; - prg_hook : Tacexpr.declaration_hook; -} - -let assumption_message id = - Flags.if_verbose message ((string_of_id id) ^ " is assumed") - -let (set_default_tactic, get_default_tactic, print_default_tactic) = - Tactic_option.declare_tactic_option "Program tactic" - -(* true = All transparent, false = Opaque if possible *) -let proofs_transparency = ref true - -let set_proofs_transparency = (:=) proofs_transparency -let get_proofs_transparency () = !proofs_transparency - -open Goptions - -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "transparency of Program obligations"; - optkey = ["Transparent";"Obligations"]; - optread = get_proofs_transparency; - optwrite = set_proofs_transparency; } - -(* true = hide obligations *) -let hide_obligations = ref false - -let set_hide_obligations = (:=) hide_obligations -let get_hide_obligations () = !hide_obligations - -open Goptions - -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "Hidding of Program obligations"; - optkey = ["Hide";"Obligations"]; - optread = get_hide_obligations; - optwrite = set_hide_obligations; } - -let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type - -let get_obligation_body expand obl = - let c = Option.get obl.obl_body in - if expand && obl.obl_status = Expand then - match kind_of_term c with - | Const c -> constant_value (Global.env ()) c - | _ -> c - else c - -let obl_substitution expand obls deps = - Intset.fold - (fun x acc -> - let xobl = obls.(x) in - let oblb = - try get_obligation_body expand xobl - with e when Errors.noncritical e -> assert(false) - in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc) - deps [] - -let subst_deps expand obls deps t = - let subst = obl_substitution expand obls deps in - Term.replace_vars (List.map (fun (n, (_, b)) -> n, b) subst) t - -let rec prod_app t n = - match kind_of_term (strip_outer_cast t) with - | Prod (_,_,b) -> subst1 n b - | LetIn (_, b, t, b') -> prod_app (subst1 b b') n - | _ -> - errorlabstrm "prod_app" - (str"Needed a product, but didn't find one" ++ fnl ()) - - -(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) -let prod_applist t nL = List.fold_left prod_app t nL - -let replace_appvars subst = - let rec aux c = - let f, l = decompose_app c in - if isVar f then - try - let c' = List.map (map_constr aux) l in - let (t, b) = List.assoc (destVar f) subst in - mkApp (delayed_force hide_obligation, - [| prod_applist t c'; applistc b c' |]) - with Not_found -> map_constr aux c - else map_constr aux c - in map_constr aux - -let subst_prog expand obls ints prg = - let subst = obl_substitution expand obls ints in - if get_hide_obligations () then - (replace_appvars subst prg.prg_body, - replace_appvars subst (Termops.refresh_universes prg.prg_type)) - else - let subst' = List.map (fun (n, (_, b)) -> n, b) subst in - (Term.replace_vars subst' prg.prg_body, - Term.replace_vars subst' (Termops.refresh_universes prg.prg_type)) - -let subst_deps_obl obls obl = - let t' = subst_deps true obls obl.obl_deps obl.obl_type in - { obl with obl_type = t' } - -module ProgMap = Map.Make(struct type t = identifier let compare = compare end) - -let map_replace k v m = ProgMap.add k v (ProgMap.remove k m) - -let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] - -let map_cardinal m = - let i = ref 0 in - ProgMap.iter (fun _ _ -> incr i) m; - !i - -exception Found of program_info - -let map_first m = - try - ProgMap.iter (fun _ v -> raise (Found v)) m; - assert(false) - with Found x -> x - -let from_prg : program_info ProgMap.t ref = ref ProgMap.empty - -let freeze () = !from_prg -let unfreeze v = from_prg := v -let init () = from_prg := ProgMap.empty - -(** Beware: if this code is dynamically loaded via dynlink after the start - of Coq, then this [init] function will not be run by [Lib.init ()]. - Luckily, here we can launch [init] at load-time. *) - -let _ = init () - -let _ = - Summary.declare_summary "program-tcc-table" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } - -let progmap_union = ProgMap.fold ProgMap.add - -let close sec = - if not (ProgMap.is_empty !from_prg) then - let keys = map_keys !from_prg in - errorlabstrm "Program" (str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++ - prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++ - (str (if List.length keys = 1 then " has " else "have ") ++ - str "unsolved obligations")) - -let input : program_info ProgMap.t -> obj = - declare_object - { (default_object "Program state") with - cache_function = (fun (na, pi) -> from_prg := pi); - load_function = (fun _ (_, pi) -> from_prg := pi); - discharge_function = (fun _ -> close "section"; None); - classify_function = (fun _ -> close "module"; Dispose) } - -open Evd - -let progmap_remove prg = - Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg)) - -let progmap_add n prg = - Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg)) - -let progmap_replace prg' = - Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg)) - -let rec intset_to = function - -1 -> Intset.empty - | n -> Intset.add n (intset_to (pred n)) - -let subst_body expand prg = - let obls, _ = prg.prg_obligations in - let ints = intset_to (pred (Array.length obls)) in - subst_prog expand obls ints prg - -let declare_definition prg = - let body, typ = subst_body true prg in - let (local, kind) = prg.prg_kind in - let ce = - { const_entry_body = body; - const_entry_secctx = None; - const_entry_type = Some typ; - const_entry_opaque = false } - in - (Command.get_declare_definition_hook ()) ce; - match local with - | Local when Lib.sections_are_opened () -> - let c = - SectionLocalDef(ce.const_entry_body,ce.const_entry_type,false) in - let _ = declare_variable prg.prg_name (Lib.cwd(),c,IsDefinition kind) in - print_message (Subtac_utils.definition_message prg.prg_name); - if Pfedit.refining () then - Flags.if_verbose msg_warning - (str"Local definition " ++ Nameops.pr_id prg.prg_name ++ - str" is not visible from current goals"); - progmap_remove prg; - VarRef prg.prg_name - | (Global|Local) -> - let c = - Declare.declare_constant - prg.prg_name (DefinitionEntry ce,IsDefinition (snd prg.prg_kind)) - in - let gr = ConstRef c in - if Impargs.is_implicit_args () || prg.prg_implicits <> [] then - Impargs.declare_manual_implicits false gr [prg.prg_implicits]; - print_message (Subtac_utils.definition_message prg.prg_name); - progmap_remove prg; - prg.prg_hook local gr; - gr - -open Pp -open Ppconstr - -let rec lam_index n t acc = - match kind_of_term t with - | Lambda (na, _, b) -> - if na = Name n then acc - else lam_index n b (succ acc) - | _ -> raise Not_found - -let compute_possible_guardness_evidences (n,_) fixbody fixtype = - match n with - | Some (loc, n) -> [lam_index n fixbody 0] - | 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 m = Term.nb_prod fixtype in - let ctx = fst (decompose_prod_n_assum m fixtype) in - list_map_i (fun i _ -> i) 0 ctx - -let declare_mutual_definition l = - let len = List.length l in - let first = List.hd l in - let fixdefs, fixtypes, fiximps = - list_split3 - (List.map (fun x -> - let subs, typ = (subst_body true x) in - let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in - let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len typ) in - x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l) - in -(* let fixdefs = List.map reduce_fix fixdefs in *) - let fixkind = Option.get first.prg_fixkind in - let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in - let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in - let (local,kind) = first.prg_kind in - let fixnames = first.prg_deps in - let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in - let indexes, fixdecls = - match fixkind with - | IsFixpoint wfl -> - let possible_indexes = - list_map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in - let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in - Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l - | IsCoFixpoint -> - None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l - in - (* Declare the recursive definitions *) - let kns = list_map4 (declare_fix kind) fixnames fixdecls fixtypes fiximps in - (* Declare notations *) - List.iter Metasyntax.add_notation_interpretation first.prg_notations; - Declare.recursive_message (fixkind<>IsCoFixpoint) indexes fixnames; - let gr = List.hd kns in - let kn = match gr with ConstRef kn -> kn | _ -> assert false in - first.prg_hook local gr; - List.iter progmap_remove l; kn - -let declare_obligation prg obl body = - let body = prg.prg_reduce body in - let ty = prg.prg_reduce obl.obl_type in - match obl.obl_status with - | Expand -> { obl with obl_body = Some body } - | Define opaque -> - let opaque = if get_proofs_transparency () then false else opaque in - let ce = - { const_entry_body = body; - const_entry_secctx = None; - const_entry_type = Some ty; - const_entry_opaque = opaque } - in - let constant = Declare.declare_constant obl.obl_name - (DefinitionEntry ce,IsProof Property) - in - if not opaque then - Auto.add_hints false [string_of_id prg.prg_name] - (Auto.HintsUnfoldEntry [EvalConstRef constant]); - print_message (Subtac_utils.definition_message obl.obl_name); - { obl with obl_body = Some (mkConst constant) } - -let init_prog_info n b t deps fixkind notations obls impls kind reduce hook = - let obls', b = - match b with - | None -> - assert(obls = [||]); - let n = Nameops.add_suffix n "_obligation" in - [| { obl_name = n; obl_body = None; - obl_location = dummy_loc, InternalHole; obl_type = t; - obl_status = Expand; obl_deps = Intset.empty; obl_tac = None } |], - mkVar n - | Some b -> - Array.mapi - (fun i (n, t, l, o, d, tac) -> - { obl_name = n ; obl_body = None; - obl_location = l; obl_type = reduce t; obl_status = o; - obl_deps = d; obl_tac = tac }) - obls, b - in - { prg_name = n ; prg_body = b; prg_type = reduce t; prg_obligations = (obls', Array.length obls'); - prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; - prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; prg_hook = hook; } - -let get_prog name = - let prg_infos = !from_prg in - match name with - Some n -> - (try ProgMap.find n prg_infos - with Not_found -> raise (NoObligations (Some n))) - | None -> - (let n = map_cardinal prg_infos in - match n with - 0 -> raise (NoObligations None) - | 1 -> map_first prg_infos - | _ -> error "More than one program with unsolved obligations") - -let get_prog_err n = - try get_prog n with NoObligations id -> pperror (explain_no_obligations id) - -let obligations_solved prg = (snd prg.prg_obligations) = 0 - -let all_programs () = - ProgMap.fold (fun k p l -> p :: l) !from_prg [] - -type progress = - | Remain of int - | Dependent - | Defined of global_reference - -let obligations_message rem = - if rem > 0 then - if rem = 1 then - Flags.if_verbose msgnl (int rem ++ str " obligation remaining") - else - Flags.if_verbose msgnl (int rem ++ str " obligations remaining") - else - Flags.if_verbose msgnl (str "No more obligations remaining") - -let update_obls prg obls rem = - let prg' = { prg with prg_obligations = (obls, rem) } in - progmap_replace prg'; - obligations_message rem; - if rem > 0 then Remain rem - else ( - match prg'.prg_deps with - | [] -> - let kn = declare_definition prg' in - progmap_remove prg'; - Defined kn - | l -> - let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in - if List.for_all (fun x -> obligations_solved x) progs then - let kn = declare_mutual_definition progs in - Defined (ConstRef kn) - else Dependent) - -let is_defined obls x = obls.(x).obl_body <> None - -let deps_remaining obls deps = - Intset.fold - (fun x acc -> - if is_defined obls x then acc - else x :: acc) - deps [] - -let dependencies obls n = - let res = ref Intset.empty in - Array.iteri - (fun i obl -> - if i <> n && Intset.mem n obl.obl_deps then - res := Intset.add i !res) - obls; - !res - -let kind_of_opacity o = - match o with - | Define false | Expand -> Subtac_utils.goal_kind - | _ -> Subtac_utils.goal_proof_kind - -let not_transp_msg = - str "Obligation should be transparent but was declared opaque." ++ spc () ++ - str"Use 'Defined' instead." - -let warn_not_transp () = ppwarn not_transp_msg -let error_not_transp () = pperror not_transp_msg - -let rec solve_obligation prg num tac = - let user_num = succ num in - let obls, rem = prg.prg_obligations in - let obl = obls.(num) in - if obl.obl_body <> None then - pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.") - else - match deps_remaining obls obl.obl_deps with - | [] -> - let obl = subst_deps_obl obls obl in - Lemmas.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type - (fun strength gr -> - let cst = match gr with ConstRef cst -> cst | _ -> assert false in - let obl = - let transparent = evaluable_constant cst (Global.env ()) in - let body = - match obl.obl_status with - | Expand -> - if not transparent then error_not_transp () - else constant_value (Global.env ()) cst - | Define opaque -> - if not opaque && not transparent then error_not_transp () - else Libnames.constr_of_global gr - in - if transparent then - Auto.add_hints true [string_of_id prg.prg_name] - (Auto.HintsUnfoldEntry [EvalConstRef cst]); - { obl with obl_body = Some body } - in - let obls = Array.copy obls in - let _ = obls.(num) <- obl in - let res = try update_obls prg obls (pred rem) - with e when Errors.noncritical e -> - pperror (Errors.print (Cerrors.process_vernac_interp_error e)) - in - match res with - | Remain n when n > 0 -> - let deps = dependencies obls num in - if deps <> Intset.empty then - ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps) - | _ -> ()); - trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ - Subtac_utils.my_print_constr (Global.env ()) obl.obl_type); - Pfedit.by (snd (get_default_tactic ())); - Option.iter (fun tac -> Pfedit.set_end_tac (Tacinterp.interp tac)) tac; - Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () - | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " - ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) - -and subtac_obligation (user_num, name, typ) tac = - let num = pred user_num in - let prg = get_prog_err name in - let obls, rem = prg.prg_obligations in - if num < Array.length obls then - let obl = obls.(num) in - match obl.obl_body with - None -> solve_obligation prg num tac - | Some r -> error "Obligation already solved" - else error (sprintf "Unknown obligation number %i" (succ num)) - - -and solve_obligation_by_tac prg obls i tac = - let obl = obls.(i) in - match obl.obl_body with - | Some _ -> false - | None -> - try - if deps_remaining obls obl.obl_deps = [] then - let obl = subst_deps_obl obls obl in - let tac = - match tac with - | Some t -> t - | None -> - match obl.obl_tac with - | Some t -> t - | None -> snd (get_default_tactic ()) - in - let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in - obls.(i) <- declare_obligation prg obl t; - true - else false - with - | Loc.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s))) - | Loc.Exc_located(_, Refiner.FailError (_, s)) - | Refiner.FailError (_, s) -> - user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s) - | Util.Anomaly _ as e -> raise e - | e when Errors.noncritical e -> false - -and solve_prg_obligations prg ?oblset tac = - let obls, rem = prg.prg_obligations in - let rem = ref rem in - let obls' = Array.copy obls in - let set = ref Intset.empty in - let p = match oblset with - | None -> (fun _ -> true) - | Some s -> set := s; - (fun i -> Intset.mem i !set) - in - let _ = - Array.iteri (fun i x -> - if p i && solve_obligation_by_tac prg obls' i tac then - let deps = dependencies obls i in - (set := Intset.union !set deps; - decr rem)) - obls' - in - update_obls prg obls' !rem - -and solve_obligations n tac = - let prg = get_prog_err n in - solve_prg_obligations prg tac - -and solve_all_obligations tac = - ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg - -and try_solve_obligation n prg tac = - let prg = get_prog prg in - let obls, rem = prg.prg_obligations in - let obls' = Array.copy obls in - if solve_obligation_by_tac prg obls' n tac then - ignore(update_obls prg obls' (pred rem)); - -and try_solve_obligations n tac = - try ignore (solve_obligations n tac) with NoObligations _ -> () - -and auto_solve_obligations n ?oblset tac : progress = - Flags.if_verbose msgnl (str "Solving obligations automatically..."); - try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent - -open Pp -let show_obligations_of_prg ?(msg=true) prg = - let n = prg.prg_name in - let obls, rem = prg.prg_obligations in - let showed = ref 5 in - if msg then msgnl (int rem ++ str " obligation(s) remaining: "); - Array.iteri (fun i x -> - match x.obl_body with - | None -> - if !showed > 0 then ( - decr showed; - msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ - str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ - hov 1 (my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ()))) - | Some _ -> ()) - obls - -let show_obligations ?(msg=true) n = - let progs = match n with - | None -> all_programs () - | Some n -> - try [ProgMap.find n !from_prg] - with Not_found -> raise (NoObligations (Some n)) - in List.iter (show_obligations_of_prg ~msg) progs - -let show_term n = - let prg = get_prog_err n in - let n = prg.prg_name in - msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++ - my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl () - ++ my_print_constr (Global.env ()) prg.prg_body) - -let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic - ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls = - Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); - let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in - let obls,_ = prg.prg_obligations in - if Array.length obls = 0 then ( - Flags.if_verbose ppnl (str "."); - let cst = declare_definition prg in - Defined cst) - else ( - let len = Array.length obls in - let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in - progmap_add n prg; - let res = auto_solve_obligations (Some n) tactic in - match res with - | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res - | _ -> res) - -let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce) - ?(hook=fun _ _ -> ()) notations fixkind = - let deps = List.map (fun (n, b, t, imps, obls) -> n) l in - List.iter - (fun (n, b, t, imps, obls) -> - let prg = init_prog_info n (Some b) t deps (Some fixkind) - notations obls imps kind reduce hook - in progmap_add n prg) l; - let _defined = - List.fold_left (fun finished x -> - if finished then finished - else - let res = auto_solve_obligations (Some x) tactic in - match res with - | Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true - | _ -> false) - false deps - in () - -let admit_obligations n = - let prg = get_prog_err n in - let obls, rem = prg.prg_obligations in - let obls = Array.copy obls in - Array.iteri - (fun i x -> - match x.obl_body with - | None -> - let x = subst_deps_obl obls x in - let kn = Declare.declare_constant x.obl_name - (ParameterEntry (None, x.obl_type,None), IsAssumption Conjectural) - in - assumption_message x.obl_name; - obls.(i) <- { x with obl_body = Some (mkConst kn) } - | Some _ -> ()) - obls; - ignore(update_obls prg obls 0) - -exception Found of int - -let array_find f arr = - try Array.iteri (fun i x -> if f x then raise (Found i)) arr; - raise Not_found - with Found i -> i - -let next_obligation n tac = - let prg = get_prog_err n in - let obls, rem = prg.prg_obligations in - let i = - try array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) obls - with Not_found -> anomaly "Could not find a solvable obligation." - in solve_obligation prg i tac diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli deleted file mode 100644 index c1d665aa..00000000 --- a/plugins/subtac/subtac_obligations.mli +++ /dev/null @@ -1,72 +0,0 @@ -open Names -open Util -open Libnames -open Evd -open Proof_type -open Vernacexpr - -type obligation_info = - (identifier * Term.types * hole_kind located * - obligation_definition_status * Intset.t * tactic option) array - (* ident, type, location, (opaque or transparent, expand or define), - dependencies, tactic to solve it *) - -type progress = (* Resolution status of a program *) - | Remain of int (* n obligations remaining *) - | Dependent (* Dependent on other definitions *) - | Defined of global_reference (* Defined as id *) - -val set_default_tactic : bool -> Tacexpr.glob_tactic_expr -> unit -val get_default_tactic : unit -> locality_flag * Proof_type.tactic -val print_default_tactic : unit -> Pp.std_ppcmds - -val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *) -val get_proofs_transparency : unit -> bool - -val add_definition : Names.identifier -> ?term:Term.constr -> Term.types -> - ?implicits:(Topconstr.explicitation * (bool * bool * bool)) list -> - ?kind:Decl_kinds.definition_kind -> - ?tactic:Proof_type.tactic -> - ?reduce:(Term.constr -> Term.constr) -> - ?hook:(Tacexpr.declaration_hook) -> obligation_info -> progress - -type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list - -type fixpoint_kind = - | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list - | IsCoFixpoint - -val add_mutual_definitions : - (Names.identifier * Term.constr * Term.types * - (Topconstr.explicitation * (bool * bool * bool)) list * obligation_info) list -> - ?tactic:Proof_type.tactic -> - ?kind:Decl_kinds.definition_kind -> - ?reduce:(Term.constr -> Term.constr) -> - ?hook:Tacexpr.declaration_hook -> - notations -> - fixpoint_kind -> unit - -val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> - Tacexpr.raw_tactic_expr option -> unit - -val next_obligation : Names.identifier option -> Tacexpr.raw_tactic_expr option -> unit - -val solve_obligations : Names.identifier option -> Proof_type.tactic option -> progress -(* Number of remaining obligations to be solved for this program *) - -val solve_all_obligations : Proof_type.tactic option -> unit - -val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic option -> unit - -val try_solve_obligations : Names.identifier option -> Proof_type.tactic option -> unit - -val show_obligations : ?msg:bool -> Names.identifier option -> unit - -val show_term : Names.identifier option -> unit - -val admit_obligations : Names.identifier option -> unit - -exception NoObligations of Names.identifier option - -val explain_no_obligations : Names.identifier option -> Pp.std_ppcmds - diff --git a/plugins/subtac/subtac_plugin.mllib b/plugins/subtac/subtac_plugin.mllib deleted file mode 100644 index a4b9d67e..00000000 --- a/plugins/subtac/subtac_plugin.mllib +++ /dev/null @@ -1,13 +0,0 @@ -Subtac_utils -Eterm -Subtac_errors -Subtac_coercion -Subtac_obligations -Subtac_cases -Subtac_pretyping_F -Subtac_pretyping -Subtac_command -Subtac_classes -Subtac -G_subtac -Subtac_plugin_mod diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml deleted file mode 100644 index 68636574..00000000 --- a/plugins/subtac/subtac_pretyping.ml +++ /dev/null @@ -1,138 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Global -open Pp -open Util -open Names -open Sign -open Evd -open Term -open Termops -open Reductionops -open Environ -open Type_errors -open Typeops -open Libnames -open Classops -open List -open Recordops -open Evarutil -open Pretype_errors -open Glob_term -open Evarconv -open Pattern - -open Subtac_coercion -open Subtac_utils -open Coqlib -open Printer -open Subtac_errors -open Eterm - -module Pretyping = Subtac_pretyping_F.SubtacPretyping_F(Subtac_coercion.Coercion) - -open Pretyping - -let _ = Pretyping.allow_anonymous_refs := true - -type recursion_info = { - arg_name: name; - arg_type: types; (* A *) - args_after : rel_context; - wf_relation: constr; (* R : A -> A -> Prop *) - wf_proof: constr; (* : well_founded R *) - f_type: types; (* f: A -> Set *) - f_fulltype: types; (* Type with argument and wf proof product first *) -} - -let my_print_rec_info env t = - str "Name: " ++ Nameops.pr_name t.arg_name ++ spc () ++ - str "Arg type: " ++ my_print_constr env t.arg_type ++ spc () ++ - str "Wf relation: " ++ my_print_constr env t.wf_relation ++ spc () ++ - str "Wf proof: " ++ my_print_constr env t.wf_proof ++ spc () ++ - str "Abbreviated Type: " ++ my_print_constr env t.f_type ++ spc () ++ - str "Full type: " ++ my_print_constr env t.f_fulltype -(* trace (str "pretype for " ++ (my_print_glob_constr env c) ++ *) -(* str " and tycon "++ my_print_tycon env tycon ++ *) -(* str " in environment: " ++ my_print_env env); *) - -let interp env isevars c tycon = - let j = pretype true tycon env isevars ([],[]) c in - let _ = isevars := Evarutil.nf_evar_map !isevars in - let evd = consider_remaining_unif_problems env !isevars in -(* let unevd = undefined_evars evd in *) - let unevd' = Typeclasses.resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~split:true ~fail:true env evd in - let unevd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~split:true ~fail:false env unevd' in - let evm = unevd' in - isevars := unevd'; - nf_evar evm j.uj_val, nf_evar evm j.uj_type - -let find_with_index x l = - let rec aux i = function - (y, _, _) as t :: tl -> if x = y then i, t else aux (succ i) tl - | [] -> raise Not_found - in aux 0 l - -open Vernacexpr - -let coqintern_constr evd env : Topconstr.constr_expr -> Glob_term.glob_constr = - Constrintern.intern_constr evd env -let coqintern_type evd env : Topconstr.constr_expr -> Glob_term.glob_constr = - Constrintern.intern_type evd env - -let env_with_binders env isevars l = - let rec aux ((env, rels) as acc) = function - Topconstr.LocalRawDef ((loc, name), def) :: tl -> - let rawdef = coqintern_constr !isevars env def in - let coqdef, deftyp = interp env isevars rawdef empty_tycon in - let reldecl = (name, Some coqdef, deftyp) in - aux (push_rel reldecl env, reldecl :: rels) tl - | Topconstr.LocalRawAssum (bl, k, typ) :: tl -> - let rawtyp = coqintern_type !isevars env typ in - let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in - let acc = - List.fold_left (fun (env, rels) (loc, name) -> - let reldecl = (name, None, coqtyp) in - (push_rel reldecl env, - reldecl :: rels)) - (env, rels) bl - in aux acc tl - | [] -> acc - in aux (env, []) l - -let subtac_process ?(is_type=false) env isevars id bl c tycon = - let c = Topconstr.abstract_constr_expr c bl in - let tycon, imps = - match tycon with - None -> empty_tycon, None - | Some t -> - let t = Topconstr.prod_constr_expr t bl in - let t = coqintern_type !isevars env t in - let imps = Implicit_quantifiers.implicits_of_glob_constr t in - let coqt, ttyp = interp env isevars t empty_tycon in - mk_tycon coqt, Some imps - in - let c = coqintern_constr !isevars env c in - let imps = match imps with - | Some i -> i - | None -> Implicit_quantifiers.implicits_of_glob_constr ~with_products:is_type c - in - let coqc, ctyp = interp env isevars c tycon in - let evm = non_instanciated_map env isevars !isevars in - let ty = nf_evar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in - evm, coqc, ty, imps - -open Subtac_obligations - -let subtac_proof kind hook env isevars id bl c tycon = - let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in - let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in - let evm' = Subtac_utils.evars_of_term evm evm' coqt in - let evars, _, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in - add_definition id ~term:def ty ~implicits:imps ~kind ~hook evars diff --git a/plugins/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli deleted file mode 100644 index fa767790..00000000 --- a/plugins/subtac/subtac_pretyping.mli +++ /dev/null @@ -1,23 +0,0 @@ -open Term -open Environ -open Names -open Sign -open Evd -open Global -open Topconstr -open Implicit_quantifiers -open Impargs - -module Pretyping : Pretyping.S - -val interp : - Environ.env -> - Evd.evar_map ref -> - Glob_term.glob_constr -> - Evarutil.type_constraint -> Term.constr * Term.constr - -val subtac_process : ?is_type:bool -> env -> evar_map ref -> identifier -> local_binder list -> - constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list - -val subtac_proof : Decl_kinds.definition_kind -> Tacexpr.declaration_hook -> env -> evar_map ref -> identifier -> local_binder list -> - constr_expr -> constr_expr option -> Subtac_obligations.progress diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml deleted file mode 100644 index 3fc35c81..00000000 --- a/plugins/subtac/subtac_pretyping_F.ml +++ /dev/null @@ -1,662 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Pp -open Compat -open Util -open Names -open Sign -open Evd -open Term -open Reductionops -open Environ -open Type_errors -open Typeops -open Libnames -open Nameops -open Classops -open List -open Recordops -open Evarutil -open Pretype_errors -open Glob_term -open Evarconv -open Pattern -open Pretyping - -(************************************************************************) -(* This concerns Cases *) -open Declarations -open Inductive -open Inductiveops - -module SubtacPretyping_F (Coercion : Coercion.S) = struct - - module Cases = Subtac_cases.Cases_F(Coercion) - - (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) - let allow_anonymous_refs = ref true - - let evd_comb0 f evdref = - let (evd',x) = f !evdref in - evdref := evd'; - x - - let evd_comb1 f evdref x = - let (evd',y) = f !evdref x in - evdref := evd'; - y - - let evd_comb2 f evdref x y = - let (evd',z) = f !evdref x y in - evdref := evd'; - z - - let evd_comb3 f evdref x y z = - let (evd',t) = f !evdref x y z in - evdref := evd'; - t - - let mt_evd = Evd.empty - - (* Utilisé pour inférer le prédicat des Cases *) - (* Semble exagérement fort *) - (* Faudra préférer une unification entre les types de toutes les clauses *) - (* et autoriser des ? ą rester dans le résultat de l'unification *) - - let evar_type_fixpoint loc env evdref lna lar vdefj = - let lt = Array.length vdefj in - if Array.length lar = lt then - for i = 0 to lt-1 do - if not (e_cumul env evdref (vdefj.(i)).uj_type - (lift lt lar.(i))) then - error_ill_typed_rec_body_loc loc env !evdref - i lna vdefj lar - done - - let check_branches_message loc env evdref ind c (explft,lft) = - for i = 0 to Array.length explft - 1 do - if not (e_cumul env evdref lft.(i) explft.(i)) then - let sigma = !evdref in - error_ill_formed_branch_loc loc env sigma c (ind,i) lft.(i) explft.(i) - done - - (* coerce to tycon if any *) - let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function - | None -> j - | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t - - let push_rels vars env = List.fold_right push_rel vars env - - (* - let evar_type_case evdref env ct pt lft p c = - let (mind,bty,rslty) = type_case_branches env ( evdref) ct pt p c - in check_branches_message evdref env mind (c,ct) (bty,lft); (mind,rslty) - *) - - let strip_meta id = (* For Grammar v7 compatibility *) - let s = string_of_id id in - if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1)) - else id - - let invert_ltac_bound_name env id0 id = - try mkRel (pi1 (Termops.lookup_rel_id id (rel_context env))) - with Not_found -> - errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++ - str " depends on pattern variable name " ++ pr_id id ++ - str " which is not bound in current context") - - let pretype_id loc env sigma (lvar,unbndltacvars) id = - let id = strip_meta id in (* May happen in tactics defined by Grammar *) - try - let (n,_,typ) = Termops.lookup_rel_id id (rel_context env) in - { uj_val = mkRel n; uj_type = lift n typ } - with Not_found -> - try - let (ids,c) = List.assoc id lvar in - let subst = List.map (invert_ltac_bound_name env id) ids in - let c = substl subst c in - { uj_val = c; uj_type = Retyping.get_type_of env sigma c } - with Not_found -> - try - let (_,_,typ) = lookup_named id env in - { uj_val = mkVar id; uj_type = typ } - with Not_found -> - try (* To build a nicer ltac error message *) - match List.assoc id unbndltacvars with - | None -> user_err_loc (loc,"", - str "variable " ++ pr_id id ++ str " should be bound to a term") - | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0 - with Not_found -> - error_var_not_found_loc loc id - - (* make a dependent predicate from an undependent one *) - - let make_dep_of_undep env (IndType (indf,realargs)) pj = - let n = List.length realargs in - let rec decomp n p = - if n=0 then p else - match kind_of_term p with - | Lambda (_,_,c) -> decomp (n-1) c - | _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1])) - in - let sign,s = decompose_prod_n n pj.uj_type in - let ind = build_dependent_inductive env indf in - let s' = mkProd (Anonymous, ind, s) in - let ccl = lift 1 (decomp n pj.uj_val) in - let ccl' = mkLambda (Anonymous, ind, ccl) in - {uj_val=Termops.it_mkLambda ccl' sign; uj_type=Termops.it_mkProd s' sign} - - (*************************************************************************) - (* Main pretyping function *) - - let pretype_ref evdref env ref = - let c = constr_of_global ref in - make_judge c (Retyping.get_type_of env Evd.empty c) - - let pretype_sort evdref = function - | GProp c -> judge_of_prop_contents c - | GType _ -> evd_comb0 judge_of_new_Type evdref - - let split_tycon_lam loc env evd tycon = - let rec real_split evd c = - let t = whd_betadeltaiota env evd c in - match kind_of_term t with - | Prod (na,dom,rng) -> evd, (na, dom, rng) - | Evar ev when not (Evd.is_defined_evar evd ev) -> - let (evd',prod) = define_evar_as_product evd ev in - let (_,dom,rng) = destProd prod in - evd',(Anonymous, dom, rng) - | _ -> error_not_product_loc loc env evd c - in - match tycon with - | None -> evd,(Anonymous,None,None) - | Some (abs, c) -> - (match abs with - | None -> - let evd', (n, dom, rng) = real_split evd c in - evd', (n, mk_tycon dom, mk_tycon rng) - | Some (init, cur) -> - evd, (Anonymous, None, Some (Some (init, succ cur), c))) - - - (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) - (* in environment [env], with existential variables [( evdref)] and *) - (* the type constraint tycon *) - let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar c = -(* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_glob_constr env c ++ *) -(* str " with tycon " ++ Evarutil.pr_tycon env tycon) *) -(* with _ -> () *) -(* in *) - let pretype = pretype resolve_tc in - let pretype_type = pretype_type resolve_tc in - let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in - match c with - | GRef (loc,ref) -> - inh_conv_coerce_to_tycon loc env evdref - (pretype_ref evdref env ref) - tycon - - | GVar (loc, id) -> - inh_conv_coerce_to_tycon loc env evdref - (pretype_id loc env !evdref lvar id) - tycon - - | GEvar (loc, ev, instopt) -> - (* Ne faudrait-il pas s'assurer que hyps est bien un - sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) - let hyps = evar_context (Evd.find !evdref ev) in - let args = match instopt with - | None -> instance_from_named_context hyps - | Some inst -> failwith "Evar subtitutions not implemented" in - let c = mkEvar (ev, args) in - let j = (Retyping.get_judgment_of env !evdref c) in - inh_conv_coerce_to_tycon loc env evdref j tycon - - | GPatVar (loc,(someta,n)) -> - anomaly "Found a pattern variable in a glob_constr to type" - - | GHole (loc,k) -> - let ty = - match tycon with - | Some (None, ty) -> ty - | None | Some _ -> - e_new_evar evdref env ~src:(loc, InternalHole) (Termops.new_Type ()) in - { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty } - - | GRec (loc,fixkind,names,bl,lar,vdef) -> - let rec type_bl env ctxt = function - [] -> ctxt - | (na,k,None,ty)::bl -> - let ty' = pretype_type empty_valcon env evdref lvar ty in - let dcl = (na,None,ty'.utj_val) in - type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl - | (na,k,Some bd,ty)::bl -> - let ty' = pretype_type empty_valcon env evdref lvar ty in - let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar ty in - let dcl = (na,Some bd'.uj_val,ty'.utj_val) in - type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in - let ctxtv = Array.map (type_bl env empty_rel_context) bl in - let larj = - array_map2 - (fun e ar -> - pretype_type empty_valcon (push_rel_context e env) evdref lvar ar) - ctxtv lar in - let lara = Array.map (fun a -> a.utj_val) larj in - let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in - let nbfix = Array.length lar in - let names = Array.map (fun id -> Name id) names in - (* Note: bodies are not used by push_rec_types, so [||] is safe *) - let newenv = - let marked_ftys = - Array.map (fun ty -> let sort = Retyping.get_type_of env !evdref ty in - mkApp (delayed_force Subtac_utils.fix_proto, [| sort; ty |])) - ftys - in - push_rec_types (names,marked_ftys,[||]) env - in - let fixi = match fixkind with GFix (vn, i) -> i | GCoFix i -> i in - let vdefj = - array_map2_i - (fun i ctxt def -> - let fty = - let ty = ftys.(i) in - if i = fixi then ( - Option.iter (fun tycon -> - evdref := Coercion.inh_conv_coerces_to loc env !evdref ftys.(i) tycon) - tycon; - nf_evar !evdref ty) - else ty - in - (* we lift nbfix times the type in tycon, because of - * the nbfix variables pushed to newenv *) - let (ctxt,ty) = - decompose_prod_n_assum (rel_context_length ctxt) - (lift nbfix fty) in - let nenv = push_rel_context ctxt newenv in - let j = pretype (mk_tycon ty) nenv evdref lvar def in - { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; - uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) - ctxtv vdef in - evar_type_fixpoint loc env evdref names ftys vdefj; - let ftys = Array.map (nf_evar !evdref) ftys in - let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in - let fixj = match fixkind with - | GFix (vn,i) -> - (* First, let's find the guard indexes. *) - (* 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 worth the effort (except for huge mutual - fixpoints ?) *) - let possible_indexes = Array.to_list (Array.mapi - (fun i (n,_) -> match n with - | Some n -> [n] - | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i)) - vn) - in - let fixdecls = (names,ftys,fdefs) in - let indexes = search_guard loc env possible_indexes fixdecls in - make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) - | GCoFix i -> - let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env cofix - with e when Errors.noncritical e -> Loc.raise loc e); - make_judge (mkCoFix cofix) ftys.(i) in - inh_conv_coerce_to_tycon loc env evdref fixj tycon - - | GSort (loc,s) -> - let s' = pretype_sort evdref s in - inh_conv_coerce_to_tycon loc env evdref s' tycon - - | GApp (loc,f,args) -> - let length = List.length args in - let ftycon = - let ty = - if length > 0 then - match tycon with - | None -> None - | Some (None, ty) -> mk_abstr_tycon length ty - | Some (Some (init, cur), ty) -> - Some (Some (length + init, length + cur), ty) - else tycon - in - match ty with - | Some (_, t) -> - if Subtac_coercion.disc_subset (whd_betadeltaiota env !evdref t) = None then ty - else None - | _ -> None - in - let fj = pretype ftycon env evdref lvar f in - let floc = loc_of_glob_constr f in - let rec apply_rec env n resj tycon = function - | [] -> resj - | c::rest -> - let argloc = loc_of_glob_constr c in - let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in - let resty = whd_betadeltaiota env !evdref resj.uj_type in - match kind_of_term resty with - | Prod (na,c1,c2) -> - Option.iter (fun ty -> evdref := - Coercion.inh_conv_coerces_to loc env !evdref resty ty) tycon; - let evd, (_, _, tycon) = split_tycon loc env !evdref tycon in - evdref := evd; - let hj = pretype (mk_tycon c1) env evdref lvar c in - let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in - apply_rec env (n+1) - { uj_val = value; - uj_type = typ } - (Option.map (fun (abs, c) -> abs, c) tycon) rest - - | _ -> - let hj = pretype empty_tycon env evdref lvar c in - error_cant_apply_not_functional_loc - (join_loc floc argloc) env !evdref - resj [hj] - in - let resj = apply_rec env 1 fj ftycon args in - let resj = - match kind_of_term (whd_evar !evdref resj.uj_val) with - | App (f,args) when isInd f or isConst f -> - let sigma = !evdref in - let c = mkApp (f,Array.map (whd_evar sigma) args) in - let t = Retyping.get_type_of env sigma c in - make_judge c t - | _ -> resj in - inh_conv_coerce_to_tycon loc env evdref resj tycon - - | GLambda(loc,name,k,c1,c2) -> - let tycon' = evd_comb1 - (fun evd tycon -> - match tycon with - | None -> evd, tycon - | Some ty -> - let evd, ty' = Coercion.inh_coerce_to_prod loc env evd ty in - evd, Some ty') - evdref tycon - in - let (name',dom,rng) = evd_comb1 (split_tycon_lam loc env) evdref tycon' in - let dom_valcon = valcon_of_tycon dom in - let j = pretype_type dom_valcon env evdref lvar c1 in - let var = (name,None,j.utj_val) in - let j' = pretype rng (push_rel var env) evdref lvar c2 in - let resj = judge_of_abstraction env name j j' in - inh_conv_coerce_to_tycon loc env evdref resj tycon - - | GProd(loc,name,k,c1,c2) -> - let j = pretype_type empty_valcon env evdref lvar c1 in - let var = (name,j.utj_val) in - let env' = Termops.push_rel_assum var env in - let j' = pretype_type empty_valcon env' evdref lvar c2 in - let resj = - try judge_of_product env name j j' - with TypeError _ as e -> Loc.raise loc e in - inh_conv_coerce_to_tycon loc env evdref resj tycon - - | GLetIn(loc,name,c1,c2) -> - let j = pretype empty_tycon env evdref lvar c1 in - let t = Termops.refresh_universes j.uj_type in - let var = (name,Some j.uj_val,t) in - let tycon = lift_tycon 1 tycon in - let j' = pretype tycon (push_rel var env) evdref lvar c2 in - { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; - uj_type = subst1 j.uj_val j'.uj_type } - - | GLetTuple (loc,nal,(na,po),c,d) -> - let cj = pretype empty_tycon env evdref lvar c in - let (IndType (indf,realargs)) = - try find_rectype env !evdref cj.uj_type - with Not_found -> - let cloc = loc_of_glob_constr c in - error_case_not_inductive_loc cloc env !evdref cj - in - let cstrs = get_constructors env indf in - if Array.length cstrs <> 1 then - user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor"); - let cs = cstrs.(0) in - if List.length nal <> cs.cs_nargs then - user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables"); - let fsign = List.map2 (fun na (_,c,t) -> (na,c,t)) - (List.rev nal) cs.cs_args in - let env_f = push_rels fsign env in - (* Make dependencies from arity signature impossible *) - let arsgn = - let arsgn,_ = get_arity env indf in - if not !allow_anonymous_refs then - List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn - else arsgn - in - let psign = (na,None,build_dependent_inductive env indf)::arsgn in - let nar = List.length arsgn in - (match po with - | Some p -> - let env_p = push_rels psign env in - let pj = pretype_type empty_valcon env_p evdref lvar p in - let ccl = nf_evar !evdref pj.utj_val in - let psign = make_arity_signature env true indf in (* with names *) - let p = it_mkLambda_or_LetIn ccl psign in - let inst = - (Array.to_list cs.cs_concl_realargs) - @[build_dependent_constructor cs] in - let lp = lift cs.cs_nargs p in - let fty = hnf_lam_applist env !evdref lp inst in - let fj = pretype (mk_tycon fty) env_f evdref lvar d in - let f = it_mkLambda_or_LetIn fj.uj_val fsign in - let v = - let mis,_ = dest_ind_family indf in - let ci = make_case_info env mis LetStyle in - mkCase (ci, p, cj.uj_val,[|f|]) in - { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } - - | None -> - let tycon = lift_tycon cs.cs_nargs tycon in - let fj = pretype tycon env_f evdref lvar d in - let f = it_mkLambda_or_LetIn fj.uj_val fsign in - let ccl = nf_evar !evdref fj.uj_type in - let ccl = - if noccur_between 1 cs.cs_nargs ccl then - lift (- cs.cs_nargs) ccl - else - error_cant_find_case_type_loc loc env !evdref - cj.uj_val in - let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in - let v = - let mis,_ = dest_ind_family indf in - let ci = make_case_info env mis LetStyle in - mkCase (ci, p, cj.uj_val,[|f|] ) - in - { uj_val = v; uj_type = ccl }) - - | GIf (loc,c,(na,po),b1,b2) -> - let cj = pretype empty_tycon env evdref lvar c in - let (IndType (indf,realargs)) = - try find_rectype env !evdref cj.uj_type - with Not_found -> - let cloc = loc_of_glob_constr c in - error_case_not_inductive_loc cloc env !evdref cj in - let cstrs = get_constructors env indf in - if Array.length cstrs <> 2 then - user_err_loc (loc,"", - str "If is only for inductive types with two constructors."); - - let arsgn = - let arsgn,_ = get_arity env indf in - if not !allow_anonymous_refs then - (* Make dependencies from arity signature impossible *) - List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn - else arsgn - in - let nar = List.length arsgn in - let psign = (na,None,build_dependent_inductive env indf)::arsgn in - let pred,p = match po with - | Some p -> - let env_p = push_rels psign env in - let pj = pretype_type empty_valcon env_p evdref lvar p in - let ccl = nf_evar !evdref pj.utj_val in - let pred = it_mkLambda_or_LetIn ccl psign in - let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in - let jtyp = inh_conv_coerce_to_tycon loc env evdref {uj_val = pred; - uj_type = typ} tycon - in - jtyp.uj_val, jtyp.uj_type - | None -> - let p = match tycon with - | Some (None, ty) -> ty - | None | Some _ -> - e_new_evar evdref env ~src:(loc,InternalHole) (Termops.new_Type ()) - in - it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in - let pred = nf_evar !evdref pred in - let p = nf_evar !evdref p in - let f cs b = - let n = rel_context_length cs.cs_args in - let pi = lift n pred in - let pi = beta_applist (pi, [build_dependent_constructor cs]) in - let csgn = - if not !allow_anonymous_refs then - List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args - else - List.map - (fun (n, b, t) -> - match n with - Name _ -> (n, b, t) - | Anonymous -> (Name (id_of_string "H"), b, t)) - cs.cs_args - in - let env_c = push_rels csgn env in - let bj = pretype (mk_tycon pi) env_c evdref lvar b in - it_mkLambda_or_LetIn bj.uj_val cs.cs_args in - let b1 = f cstrs.(0) b1 in - let b2 = f cstrs.(1) b2 in - let v = - let mis,_ = dest_ind_family indf in - let ci = make_case_info env mis IfStyle in - mkCase (ci, pred, cj.uj_val, [|b1;b2|]) - in - { uj_val = v; uj_type = p } - - | GCases (loc,sty,po,tml,eqns) -> - Cases.compile_cases loc sty - ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref) - tycon env (* loc *) (po,tml,eqns) - - | GCast (loc,c,k) -> - let cj = - match k with - CastCoerce -> - let cj = pretype empty_tycon env evdref lvar c in - evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj - | CastConv (k,t) -> - let tj = pretype_type empty_valcon env evdref lvar t in - let cj = pretype (mk_tycon tj.utj_val) env evdref lvar c in - let v = mkCast (cj.uj_val, k, tj.utj_val) in - { uj_val = v; uj_type = tj.utj_val } - in - inh_conv_coerce_to_tycon loc env evdref cj tycon - - (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) - and pretype_type resolve_tc valcon env evdref lvar = function - | GHole loc -> - (match valcon with - | Some v -> - let s = - let sigma = !evdref in - let t = Retyping.get_type_of env sigma v in - match kind_of_term (whd_betadeltaiota env sigma t) with - | Sort s -> s - | Evar ev when is_Type (existential_type sigma ev) -> - evd_comb1 (define_evar_as_sort) evdref ev - | _ -> anomaly "Found a type constraint which is not a type" - in - { utj_val = v; - utj_type = s } - | None -> - let s = Termops.new_Type_sort () in - { utj_val = e_new_evar evdref env ~src:loc (mkSort s); - utj_type = s}) - | c -> - let j = pretype resolve_tc empty_tycon env evdref lvar c in - let loc = loc_of_glob_constr c in - let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in - match valcon with - | None -> tj - | Some v -> - if e_cumul env evdref v tj.utj_val then tj - else - error_unexpected_type_loc - (loc_of_glob_constr c) env !evdref tj.utj_val v - - let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c = - let c' = match kind with - | OfType exptyp -> - let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in - (pretype resolve_classes tycon env evdref lvar c).uj_val - | IsType -> - (pretype_type resolve_classes empty_valcon env evdref lvar c).utj_val - in - if resolve_classes then - (try - evdref := Typeclasses.resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations - ~split:true ~fail:true env !evdref; - evdref := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars - ~split:true ~fail:false env !evdref - with e when Errors.noncritical e -> - if fail_evar then raise e else ()); - evdref := consider_remaining_unif_problems env !evdref; - let c = if expand_evar then nf_evar !evdref c' else c' in - if fail_evar then check_evars env Evd.empty !evdref c; - c - - (* TODO: comment faire remonter l'information si le typage a resolu des - variables du sigma original. il faudrait que la fonction de typage - retourne aussi le nouveau sigma... - *) - - let understand_judgment sigma env c = - let evdref = ref (create_evar_defs sigma) in - let j = pretype true empty_tycon env evdref ([],[]) c in - let evd = consider_remaining_unif_problems env !evdref in - let j = j_nf_evar evd j in - check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); - j - - let understand_judgment_tcc evdref env c = - let j = pretype true empty_tycon env evdref ([],[]) c in - j_nf_evar !evdref j - - (* Raw calls to the unsafe inference machine: boolean says if we must - fail on unresolved evars; the unsafe_judgment list allows us to - extend env with some bindings *) - - let ise_pretype_gen expand_evar fail_evar resolve_classes sigma env lvar kind c = - let evdref = ref (Evd.create_evar_defs sigma) in - let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in - !evdref, c - - (** Entry points of the high-level type synthesis algorithm *) - - let understand_gen kind sigma env c = - snd (ise_pretype_gen true true true sigma env ([],[]) kind c) - - let understand sigma env ?expected_type:exptyp c = - snd (ise_pretype_gen true true true sigma env ([],[]) (OfType exptyp) c) - - let understand_type sigma env c = - snd (ise_pretype_gen true false true sigma env ([],[]) IsType c) - - let understand_ltac ?(resolve_classes=false) expand_evar sigma env lvar kind c = - ise_pretype_gen expand_evar false resolve_classes sigma env lvar kind c - - let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c = - ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c - - let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c = - pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c -end - -module Default : S = SubtacPretyping_F(Coercion.Default) diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml deleted file mode 100644 index e32bb9e0..00000000 --- a/plugins/subtac/subtac_utils.ml +++ /dev/null @@ -1,476 +0,0 @@ -(** -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *) - -open Evd -open Libnames -open Coqlib -open Term -open Names -open Util - -let ($) f x = f x - -(****************************************************************************) -(* Library linking *) - -let contrib_name = "Program" - -let subtac_dir = [contrib_name] -let fixsub_module = subtac_dir @ ["Wf"] -let utils_module = subtac_dir @ ["Utils"] -let tactics_module = subtac_dir @ ["Tactics"] -let init_constant dir s () = gen_constant contrib_name dir s -let init_reference dir s () = gen_reference contrib_name dir s - -let safe_init_constant md name () = - check_required_library ("Coq"::md); - init_constant md name () - -let ex_pi1 = init_constant utils_module "ex_pi1" -let ex_pi2 = init_constant utils_module "ex_pi2" - -let make_ref l s = init_reference l s -let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded" -let acc_ref = make_ref ["Init";"Wf"] "Acc" -let acc_inv_ref = make_ref ["Init";"Wf"] "Acc_inv" -let fix_sub_ref = make_ref fixsub_module "Fix_sub" -let measure_on_R_ref = make_ref fixsub_module "MR" -let fix_measure_sub_ref = make_ref fixsub_module "Fix_measure_sub" -let refl_ref = make_ref ["Init";"Logic"] "refl_equal" - -let make_ref s = Qualid (dummy_loc, qualid_of_string s) -let lt_ref = make_ref "Init.Peano.lt" -let sig_ref = make_ref "Init.Specif.sig" -let proj1_sig_ref = make_ref "Init.Specif.proj1_sig" -let proj2_sig_ref = make_ref "Init.Specif.proj2_sig" - -let build_sig () = - { proj1 = init_constant ["Init"; "Specif"] "proj1_sig" (); - proj2 = init_constant ["Init"; "Specif"] "proj2_sig" (); - elim = init_constant ["Init"; "Specif"] "sig_rec" (); - intro = init_constant ["Init"; "Specif"] "exist" (); - typ = init_constant ["Init"; "Specif"] "sig" () } - -let sig_ = build_sig - -let fix_proto = safe_init_constant tactics_module "fix_proto" - -let hide_obligation = safe_init_constant tactics_module "obligation" - -let eq_ind = init_constant ["Init"; "Logic"] "eq" -let eq_rec = init_constant ["Init"; "Logic"] "eq_rec" -let eq_rect = init_constant ["Init"; "Logic"] "eq_rect" -let eq_refl = init_constant ["Init"; "Logic"] "refl_equal" -let eq_ind_ref = init_reference ["Init"; "Logic"] "eq" -let refl_equal_ref = init_reference ["Init"; "Logic"] "refl_equal" - -let not_ref = init_constant ["Init"; "Logic"] "not" - -let and_typ = Coqlib.build_coq_and - -let eqdep_ind = init_constant [ "Logic";"Eqdep"] "eq_dep" -let eqdep_rec = init_constant ["Logic";"Eqdep"] "eq_dep_rec" -let eqdep_ind_ref = init_reference [ "Logic";"Eqdep"] "eq_dep" -let eqdep_intro_ref = init_reference [ "Logic";"Eqdep"] "eq_dep_intro" - -let jmeq_ind = - safe_init_constant ["Logic";"JMeq"] "JMeq" - -let jmeq_rec = - init_constant ["Logic";"JMeq"] "JMeq_rec" - -let jmeq_refl = - init_constant ["Logic";"JMeq"] "JMeq_refl" - -let ex_ind = init_constant ["Init"; "Logic"] "ex" -let ex_intro = init_reference ["Init"; "Logic"] "ex_intro" - -let proj1 = init_constant ["Init"; "Logic"] "proj1" -let proj2 = init_constant ["Init"; "Logic"] "proj2" - -let existS = build_sigma_type - -let prod = build_prod - - -(* orders *) -let well_founded = init_constant ["Init"; "Wf"] "well_founded" -let fix = init_constant ["Init"; "Wf"] "Fix" -let acc = init_constant ["Init"; "Wf"] "Acc" -let acc_inv = init_constant ["Init"; "Wf"] "Acc_inv" - -let extconstr = Constrextern.extern_constr true (Global.env ()) -let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s) - -open Pp - -let my_print_constr = Termops.print_constr_env -let my_print_constr_expr = Ppconstr.pr_constr_expr -let my_print_rel_context env ctx = Printer.pr_rel_context env ctx -let my_print_context = Termops.print_rel_context -let my_print_named_context = Termops.print_named_context -let my_print_env = Termops.print_env -let my_print_glob_constr = Printer.pr_glob_constr_env -let my_print_evardefs = Evd.pr_evar_map None - -let my_print_tycon_type = Evarutil.pr_tycon_type - -let debug_level = 2 - -let debug_on = true - -let debug n s = - if debug_on then - if !Flags.debug && n >= debug_level then - msgnl s - else () - else () - -let debug_msg n s = - if debug_on then - if !Flags.debug && n >= debug_level then s - else mt () - else mt () - -let trace s = - if debug_on then - if !Flags.debug && debug_level > 0 then msgnl s - else () - else () - -let rec pp_list f = function - [] -> mt() - | x :: y -> f x ++ spc () ++ pp_list f y - -let wf_relations = Hashtbl.create 10 - -let std_relations () = - let add k v = Hashtbl.add wf_relations k v in - add (init_constant ["Init"; "Peano"] "lt" ()) - (init_constant ["Arith"; "Wf_nat"] "lt_wf") - -let std_relations = Lazy.lazy_from_fun std_relations - -type binders = Topconstr.local_binder list - -let app_opt c e = - match c with - Some constr -> constr e - | None -> e - -let print_args env args = - Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "") - -let make_existential loc ?(opaque = Define true) env isevars c = - Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c - -let no_goals_or_obligations = function - | GoalEvar | QuestionMark _ -> false - | _ -> true - -let make_existential_expr loc env c = - let key = Evarutil.new_untyped_evar () in - let evar = Topconstr.CEvar (loc, key, None) in - debug 2 (str "Constructed evar " ++ int key); - evar - -let string_of_hole_kind = function - | ImplicitArg _ -> "ImplicitArg" - | BinderType _ -> "BinderType" - | QuestionMark _ -> "QuestionMark" - | CasesType -> "CasesType" - | InternalHole -> "InternalHole" - | TomatchTypeParameter _ -> "TomatchTypeParameter" - | GoalEvar -> "GoalEvar" - | ImpossibleCase -> "ImpossibleCase" - | MatchingVar _ -> "MatchingVar" - -let evars_of_term evc init c = - let rec evrec acc c = - match kind_of_term c with - | Evar (n, _) when Evd.mem evc n -> Evd.add acc n (Evd.find evc n) - | Evar (n, _) -> assert(false) - | _ -> fold_constr evrec acc c - in - evrec init c - -let non_instanciated_map env evd evm = - List.fold_left - (fun evm (key, evi) -> - let (loc,k) = evar_source key !evd in - debug 2 (str "evar " ++ int key ++ str " has kind " ++ - str (string_of_hole_kind k)); - match k with - | QuestionMark _ -> Evd.add evm key evi - | ImplicitArg (_,_,false) -> Evd.add evm key evi - | _ -> - debug 2 (str " and is an implicit"); - Pretype_errors.error_unsolvable_implicit loc env evm (Evarutil.nf_evar_info evm evi) k None) - Evd.empty (Evarutil.non_instantiated evm) - -let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition -let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition - -let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma -let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma - -let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint -let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint - -open Tactics -open Tacticals - -let filter_map f l = - let rec aux acc = function - hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl - | None -> aux acc tl) - | [] -> List.rev acc - in aux [] l - -let build_dependent_sum l = - let rec aux names conttac conttype = function - (n, t) :: ((_ :: _) as tl) -> - let hyptype = substl names t in - trace (spc () ++ str ("treating evar " ^ string_of_id n)); - (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype) - with e when Errors.noncritical e -> ()); - let tac = assert_tac (Name n) hyptype in - let conttac = - (fun cont -> - conttac - (tclTHENS tac - ([intros; - (tclTHENSEQ - [constructor_tac false (Some 1) 1 - (Glob_term.ImplicitBindings [mkVar n]); - cont]); - ]))) - in - let conttype = - (fun typ -> - let tex = mkLambda (Name n, t, typ) in - conttype - (mkApp (ex_ind (), [| t; tex |]))) - in - aux (mkVar n :: names) conttac conttype tl - | (n, t) :: [] -> - (conttac intros, conttype t) - | [] -> raise (Invalid_argument "build_dependent_sum") - in aux [] identity identity (List.rev l) - -open Proof_type -open Tacexpr - -let mkProj1 a b c = - mkApp (delayed_force proj1, [| a; b; c |]) - -let mkProj2 a b c = - mkApp (delayed_force proj2, [| a; b; c |]) - -let mk_ex_pi1 a b c = - mkApp (delayed_force ex_pi1, [| a; b; c |]) - -let mk_ex_pi2 a b c = - mkApp (delayed_force ex_pi2, [| a; b; c |]) - -let mkSubset name typ prop = - mkApp ((delayed_force sig_).typ, - [| typ; mkLambda (name, typ, prop) |]) - -let mk_eq typ x y = mkApp (delayed_force eq_ind, [| typ; x ; y |]) -let mk_eq_refl typ x = mkApp (delayed_force eq_refl, [| typ; x |]) -let mk_JMeq typ x typ' y = mkApp (delayed_force jmeq_ind, [| typ; x ; typ'; y |]) -let mk_JMeq_refl typ x = mkApp (delayed_force jmeq_refl, [| typ; x |]) - -let unsafe_fold_right f = function - hd :: tl -> List.fold_right f tl hd - | [] -> raise (Invalid_argument "unsafe_fold_right") - -let mk_conj l = - let conj_typ = delayed_force and_typ in - unsafe_fold_right - (fun c conj -> - mkApp (conj_typ, [| c ; conj |])) - l - -let mk_not c = - let notc = delayed_force not_ref in - mkApp (notc, [| c |]) - -let and_tac l hook = - let andc = Coqlib.build_coq_and () in - let rec aux ((accid, goal, tac, extract) as acc) = function - | [] -> (* Singleton *) acc - - | (id, x, elgoal, eltac) :: tl -> - let tac' = tclTHEN simplest_split (tclTHENLIST [tac; eltac]) in - let proj = fun c -> mkProj2 goal elgoal c in - let extract = List.map (fun (id, x, y, f) -> (id, x, y, (fun c -> f (mkProj1 goal elgoal c)))) extract in - aux ((string_of_id id) ^ "_" ^ accid, mkApp (andc, [| goal; elgoal |]), tac', - (id, x, elgoal, proj) :: extract) tl - - in - let and_proof_id, and_goal, and_tac, and_extract = - match l with - | [] -> raise (Invalid_argument "and_tac: empty list of goals") - | (hdid, x, hdg, hdt) :: tl -> - aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl - in - let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in - Lemmas.start_proof and_proofid goal_kind and_goal - (hook (fun c -> List.map (fun (id, x, t, f) -> (id, x, t, f c)) and_extract)); - trace (str "Started and proof"); - Pfedit.by and_tac; - trace (str "Applied and tac") - - -let destruct_ex ext ex = - let rec aux c acc = - match kind_of_term c with - App (f, args) -> - (match kind_of_term f with - Ind i when i = Term.destInd (delayed_force ex_ind) && Array.length args = 2 -> - let (dom, rng) = - try (args.(0), args.(1)) - with e when Errors.noncritical e -> assert(false) - in - let pi1 = (mk_ex_pi1 dom rng acc) in - let rng_body = - match kind_of_term rng with - Lambda (_, _, t) -> subst1 pi1 t - | t -> rng - in - pi1 :: aux rng_body (mk_ex_pi2 dom rng acc) - | _ -> [acc]) - | _ -> [acc] - in aux ex ext - -open Glob_term - -let id_of_name = function - Name n -> n - | Anonymous -> raise (Invalid_argument "id_of_name") - -let definition_message id = - Nameops.pr_id id ++ str " is defined" - -let recursive_message v = - match Array.length v with - | 0 -> error "no recursive definition" - | 1 -> (Printer.pr_constant (Global.env ()) v.(0) ++ str " is recursively defined") - | _ -> hov 0 (prvect_with_sep pr_comma (Printer.pr_constant (Global.env ())) v ++ - spc () ++ str "are recursively defined") - -let print_message m = - Flags.if_verbose ppnl m - -(* Solve an obligation using tactics, return the corresponding proof term *) -let solve_by_tac evi t = - let id = id_of_string "H" in - try - Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl - (fun _ _ -> ()); - Pfedit.by (tclCOMPLETE t); - let _,(const,_,_,_) = Pfedit.cook_proof ignore in - Pfedit.delete_current_proof (); - Inductiveops.control_only_guard (Global.env ()) - const.Entries.const_entry_body; - const.Entries.const_entry_body - with reraise -> - Pfedit.delete_current_proof(); - raise reraise - -(* let apply_tac t goal = t goal *) - -(* let solve_by_tac evi t = *) -(* let ev = 1 in *) -(* let evm = Evd.add Evd.empty ev evi in *) -(* let goal = {it = evi; sigma = evm } in *) -(* let (res, valid) = apply_tac t goal in *) -(* if res.it = [] then *) -(* let prooftree = valid [] in *) -(* let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *) -(* if obls = [] then proofterm *) -(* else raise Exit *) -(* else raise Exit *) - -let rec string_of_list sep f = function - [] -> "" - | x :: [] -> f x - | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl - -let string_of_intset d = - string_of_list "," string_of_int (Intset.elements d) - -(**********************************************************) -(* Pretty-printing *) -open Printer -open Ppconstr -open Nameops -open Evd - -let pr_meta_map evd = - let ml = meta_list evd in - let pr_name = function - Name id -> str"[" ++ pr_id id ++ str"]" - | _ -> mt() in - let pr_meta_binding = function - | (mv,Cltyp (na,b)) -> - hov 0 - (pr_meta mv ++ pr_name na ++ str " : " ++ - Termops.print_constr b.rebus ++ fnl ()) - | (mv,Clval(na,b,_)) -> - hov 0 - (pr_meta mv ++ pr_name na ++ str " := " ++ - Termops.print_constr (fst b).rebus ++ fnl ()) - in - prlist pr_meta_binding ml - -let pr_idl idl = prlist_with_sep pr_spc pr_id idl - -let pr_evar_info evi = - let phyps = - (*pr_idl (List.rev (ids_of_named_context (evar_context evi))) *) - Printer.pr_named_context (Global.env()) (evar_context evi) - in - let pty = Termops.print_constr evi.evar_concl in - let pb = - match evi.evar_body with - | Evar_empty -> mt () - | Evar_defined c -> spc() ++ str"=> " ++ Termops.print_constr c - in - hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]") - -let pr_evar_map sigma = - h 0 - (prlist_with_sep pr_fnl - (fun (ev,evi) -> - h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi)) - (to_list sigma)) - -let pr_constraints pbs = - h 0 - (prlist_with_sep pr_fnl (fun (pbty,t1,t2) -> - Termops.print_constr t1 ++ spc() ++ - str (match pbty with - | Reduction.CONV -> "==" - | Reduction.CUMUL -> "<=") ++ - spc() ++ Termops.print_constr t2) pbs) - -let pr_evar_map evd = - let pp_evm = - let evars = evd in - if evars = empty then mt() else - str"EVARS:"++brk(0,1)++pr_evar_map evars++fnl() in - let pp_met = - if meta_list evd = [] then mt() else - str"METAS:"++brk(0,1)++pr_meta_map evd in - v 0 (pp_evm ++ pp_met) - -let contrib_tactics_path = - make_dirpath (List.map id_of_string ["Tactics";contrib_name;"Coq"]) - -let tactics_tac s = - lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s)) - -let tactics_call tac args = - TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args)) diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli deleted file mode 100644 index 112b1795..00000000 --- a/plugins/subtac/subtac_utils.mli +++ /dev/null @@ -1,131 +0,0 @@ -open Term -open Libnames -open Coqlib -open Environ -open Pp -open Evd -open Decl_kinds -open Topconstr -open Glob_term -open Util -open Evarutil -open Names -open Sign - -val ($) : ('a -> 'b) -> 'a -> 'b -val contrib_name : string -val subtac_dir : string list -val fixsub_module : string list -val init_constant : string list -> string -> constr delayed -val init_reference : string list -> string -> global_reference delayed -val well_founded_ref : global_reference delayed -val acc_ref : global_reference delayed -val acc_inv_ref : global_reference delayed -val fix_sub_ref : global_reference delayed -val measure_on_R_ref : global_reference delayed -val fix_measure_sub_ref : global_reference delayed -val refl_ref : global_reference delayed -val lt_ref : reference -val sig_ref : reference -val proj1_sig_ref : reference -val proj2_sig_ref : reference -val build_sig : unit -> coq_sigma_data -val sig_ : coq_sigma_data delayed - -val fix_proto : constr delayed - -val hide_obligation : constr delayed - -val eq_ind : constr delayed -val eq_rec : constr delayed -val eq_rect : constr delayed -val eq_refl : constr delayed - -val not_ref : constr delayed -val and_typ : constr delayed - -val eqdep_ind : constr delayed -val eqdep_rec : constr delayed - -val jmeq_ind : constr delayed -val jmeq_rec : constr delayed -val jmeq_refl : constr delayed - -val existS : coq_sigma_data delayed -val prod : coq_sigma_data delayed - -val well_founded : constr delayed -val fix : constr delayed -val acc : constr delayed -val acc_inv : constr delayed -val extconstr : constr -> constr_expr -val extsort : sorts -> constr_expr - -val my_print_constr : env -> constr -> std_ppcmds -val my_print_constr_expr : constr_expr -> std_ppcmds -val my_print_evardefs : evar_map -> std_ppcmds -val my_print_context : env -> std_ppcmds -val my_print_rel_context : env -> rel_context -> std_ppcmds -val my_print_named_context : env -> std_ppcmds -val my_print_env : env -> std_ppcmds -val my_print_glob_constr : env -> glob_constr -> std_ppcmds -val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds - - -val debug : int -> std_ppcmds -> unit -val debug_msg : int -> std_ppcmds -> std_ppcmds -val trace : std_ppcmds -> unit -val wf_relations : (constr, constr delayed) Hashtbl.t - -type binders = local_binder list -val app_opt : ('a -> 'a) option -> 'a -> 'a -val print_args : env -> constr array -> std_ppcmds -val make_existential : loc -> ?opaque:obligation_definition_status -> - env -> evar_map ref -> types -> constr -val no_goals_or_obligations : Typeclasses.evar_filter -val make_existential_expr : loc -> 'a -> 'b -> constr_expr -val string_of_hole_kind : hole_kind -> string -val evars_of_term : evar_map -> evar_map -> constr -> evar_map -val non_instanciated_map : env -> evar_map ref -> evar_map -> evar_map -val global_kind : logical_kind -val goal_kind : locality * goal_object_kind -val global_proof_kind : logical_kind -val goal_proof_kind : locality * goal_object_kind -val global_fix_kind : logical_kind -val goal_fix_kind : locality * goal_object_kind - -val mkSubset : name -> constr -> constr -> constr -val mkProj1 : constr -> constr -> constr -> constr -val mkProj1 : constr -> constr -> constr -> constr -val mk_ex_pi1 : constr -> constr -> constr -> constr -val mk_ex_pi1 : constr -> constr -> constr -> constr -val mk_eq : types -> constr -> constr -> types -val mk_eq_refl : types -> constr -> constr -val mk_JMeq : types -> constr-> types -> constr -> types -val mk_JMeq_refl : types -> constr -> constr -val mk_conj : types list -> types -val mk_not : types -> types - -val build_dependent_sum : (identifier * types) list -> Proof_type.tactic * types -val and_tac : (identifier * 'a * constr * Proof_type.tactic) list -> - ((constr -> (identifier * 'a * constr * constr) list) -> Tacexpr.declaration_hook) -> unit - -val destruct_ex : constr -> constr -> constr list - -val id_of_name : name -> identifier - -val definition_message : identifier -> std_ppcmds -val recursive_message : constant array -> std_ppcmds - -val print_message : std_ppcmds -> unit - -val solve_by_tac : evar_info -> Tacmach.tactic -> constr - -val string_of_list : string -> ('a -> string) -> 'a list -> string -val string_of_intset : Intset.t -> string - -val pr_evar_map : evar_map -> Pp.std_ppcmds - -val tactics_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr - -val pp_list : ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds diff --git a/plugins/subtac/test/ListDep.v b/plugins/subtac/test/ListDep.v deleted file mode 100644 index e3dbd127..00000000 --- a/plugins/subtac/test/ListDep.v +++ /dev/null @@ -1,49 +0,0 @@ -(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) -Require Import List. -Require Import Coq.Program.Program. - -Set Implicit Arguments. - -Definition sub_list (A : Set) (l' l : list A) := (forall v, In v l' -> In v l) /\ length l' <= length l. - -Lemma sub_list_tl : forall A : Set, forall x (l l' : list A), sub_list (x :: l) l' -> sub_list l l'. -Proof. - intros. - inversion H. - split. - intros. - apply H0. - auto with datatypes. - auto with arith. -Qed. - -Section Map_DependentRecursor. - Variable U V : Set. - Variable l : list U. - Variable f : { x : U | In x l } -> V. - - Obligations Tactic := unfold sub_list in * ; - program_simpl ; intuition. - - Program Fixpoint map_rec ( l' : list U | sub_list l' l ) - { measure length l' } : { r : list V | length r = length l' } := - match l' with - | nil => nil - | cons x tl => let tl' := map_rec tl in - f x :: tl' - end. - - Next Obligation. - destruct_call map_rec. - simpl in *. - subst l'. - simpl ; auto with arith. - Qed. - - Program Definition map : list V := map_rec l. - -End Map_DependentRecursor. - -Extraction map. -Extraction map_rec. - diff --git a/plugins/subtac/test/ListsTest.v b/plugins/subtac/test/ListsTest.v deleted file mode 100644 index 2cea0841..00000000 --- a/plugins/subtac/test/ListsTest.v +++ /dev/null @@ -1,99 +0,0 @@ -(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) -Require Import Coq.Program.Program. -Require Import List. - -Set Implicit Arguments. - -Section Accessors. - Variable A : Set. - - Program Definition myhd : forall (l : list A | length l <> 0), A := - fun l => - match l with - | nil => ! - | hd :: tl => hd - end. - - Program Definition mytail (l : list A | length l <> 0) : list A := - match l with - | nil => ! - | hd :: tl => tl - end. -End Accessors. - -Program Definition test_hd : nat := myhd (cons 1 nil). - -(*Eval compute in test_hd*) -(*Program Definition test_tail : list A := mytail nil.*) - -Section app. - Variable A : Set. - - Program Fixpoint app (l : list A) (l' : list A) { struct l } : - { r : list A | length r = length l + length l' } := - match l with - | nil => l' - | hd :: tl => hd :: (tl ++ l') - end - where "x ++ y" := (app x y). - - Next Obligation. - intros. - destruct_call app ; program_simpl. - Defined. - - Program Lemma app_id_l : forall l : list A, l = nil ++ l. - Proof. - simpl ; auto. - Qed. - - Program Lemma app_id_r : forall l : list A, l = l ++ nil. - Proof. - induction l ; simpl in * ; auto. - rewrite <- IHl ; auto. - Qed. - -End app. - -Extraction app. - -Section Nth. - - Variable A : Set. - - Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A := - match n, l with - | 0, hd :: _ => hd - | S n', _ :: tl => nth tl n' - | _, nil => ! - end. - - Next Obligation. - Proof. - simpl in *. auto with arith. - Defined. - - Next Obligation. - Proof. - inversion H. - Qed. - - Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := - match l, n with - | hd :: _, 0 => hd - | _ :: tl, S n' => nth' tl n' - | nil, _ => ! - end. - Next Obligation. - Proof. - simpl in *. auto with arith. - Defined. - - Next Obligation. - Proof. - intros. - inversion H. - Defined. - -End Nth. - diff --git a/plugins/subtac/test/Mutind.v b/plugins/subtac/test/Mutind.v deleted file mode 100644 index 01e2d75f..00000000 --- a/plugins/subtac/test/Mutind.v +++ /dev/null @@ -1,20 +0,0 @@ -Require Import List. - -Program Fixpoint f a : { x : nat | x > 0 } := - match a with - | 0 => 1 - | S a' => g a a' - end -with g a b : { x : nat | x > 0 } := - match b with - | 0 => 1 - | S b' => f b' - end. - -Check f. -Check g. - - - - - diff --git a/plugins/subtac/test/Test1.v b/plugins/subtac/test/Test1.v deleted file mode 100644 index 7e0755d5..00000000 --- a/plugins/subtac/test/Test1.v +++ /dev/null @@ -1,16 +0,0 @@ -Program Definition test (a b : nat) : { x : nat | x = a + b } := - ((a + b) : { x : nat | x = a + b }). -Proof. -intros. -reflexivity. -Qed. - -Print test. - -Require Import List. - -Program hd_opt (l : list nat) : { x : nat | x <> 0 } := - match l with - nil => 1 - | a :: l => a - end. diff --git a/plugins/subtac/test/euclid.v b/plugins/subtac/test/euclid.v deleted file mode 100644 index 97c3d941..00000000 --- a/plugins/subtac/test/euclid.v +++ /dev/null @@ -1,24 +0,0 @@ -Require Import Coq.Program.Program. -Require Import Coq.Arith.Compare_dec. -Notation "( x & y )" := (existS _ x y) : core_scope. - -Require Import Omega. - -Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf lt a} : - { q : nat & { r : nat | a = b * q + r /\ r < b } } := - if le_lt_dec b a then let (q', r) := euclid (a - b) b in - (S q' & r) - else (O & a). - -Next Obligation. - assert(b * S q' = b * q' + b) by auto with arith ; omega. -Defined. - -Program Definition test_euclid : (prod nat nat) := let (q, r) := euclid 4 2 in (q, q). - -Eval lazy beta zeta delta iota in test_euclid. - -Program Definition testsig (a : nat) : { x : nat & { y : nat | x < y } } := - (a & S a). - -Check testsig. diff --git a/plugins/subtac/test/id.v b/plugins/subtac/test/id.v deleted file mode 100644 index 9ae11088..00000000 --- a/plugins/subtac/test/id.v +++ /dev/null @@ -1,46 +0,0 @@ -Require Coq.Arith.Arith. - -Require Import Coq.subtac.Utils. -Program Fixpoint id (n : nat) : { x : nat | x = n } := - match n with - | O => O - | S p => S (id p) - end. -intros ; auto. - -pose (subset_simpl (id p)). -simpl in e. -unfold p0. -rewrite e. -auto. -Defined. - -Check id. -Print id. -Extraction id. - -Axiom le_gt_dec : forall n m, { n <= m } + { n > m }. -Require Import Omega. - -Program Fixpoint id_if (n : nat) { wf n lt }: { x : nat | x = n } := - if le_gt_dec n 0 then 0 - else S (id_if (pred n)). -intros. -auto with arith. -intros. -pose (subset_simpl (id_if (pred n))). -simpl in e. -rewrite e. -induction n ; auto with arith. -Defined. - -Print id_if_instance. -Extraction id_if_instance. - -Notation "( x & y )" := (@existS _ _ x y) : core_scope. - -Program Definition testsig ( a : nat ) : { x : nat & { y : nat | x = y }} := - (a & a). -intros. -auto. -Qed. diff --git a/plugins/subtac/test/measure.v b/plugins/subtac/test/measure.v deleted file mode 100644 index 4f938f4f..00000000 --- a/plugins/subtac/test/measure.v +++ /dev/null @@ -1,20 +0,0 @@ -Notation "( x & y )" := (@existS _ _ x y) : core_scope. -Unset Printing All. -Require Import Coq.Arith.Compare_dec. - -Require Import Coq.Program.Program. - -Fixpoint size (a : nat) : nat := - match a with - 0 => 1 - | S n => S (size n) - end. - -Program Fixpoint test_measure (a : nat) {measure size a} : nat := - match a with - | S (S n) => S (test_measure n) - | 0 | S 0 => a - end. - -Check test_measure. -Print test_measure.
\ No newline at end of file diff --git a/plugins/subtac/test/rec.v b/plugins/subtac/test/rec.v deleted file mode 100644 index aaefd8cc..00000000 --- a/plugins/subtac/test/rec.v +++ /dev/null @@ -1,65 +0,0 @@ -Require Import Coq.Arith.Arith. -Require Import Lt. -Require Import Omega. - -Axiom lt_ge_dec : forall x y : nat, { x < y } + { x >= y }. -(*Proof. - intros. - elim (le_lt_dec y x) ; intros ; auto with arith. -Defined. -*) -Require Import Coq.subtac.FixSub. -Require Import Wf_nat. - -Lemma preda_lt_a : forall a, 0 < a -> pred a < a. -auto with arith. -Qed. - -Program Fixpoint id_struct (a : nat) : nat := - match a with - 0 => 0 - | S n => S (id_struct n) - end. - -Check struct_rec. - - if (lt_ge_dec O a) - then S (wfrec (pred a)) - else O. - -Program Fixpoint wfrec (a : nat) { wf a lt } : nat := - if (lt_ge_dec O a) - then S (wfrec (pred a)) - else O. -intros. -apply preda_lt_a ; auto. - -Defined. - -Extraction wfrec. -Extraction Inline proj1_sig. -Extract Inductive bool => "bool" [ "true" "false" ]. -Extract Inductive sumbool => "bool" [ "true" "false" ]. -Extract Inlined Constant lt_ge_dec => "<". - -Extraction wfrec. -Extraction Inline lt_ge_dec le_lt_dec. -Extraction wfrec. - - -Program Fixpoint structrec (a : nat) { wf a lt } : nat := - match a with - S n => S (structrec n) - | 0 => 0 - end. -intros. -unfold n0. -omega. -Defined. - -Print structrec. -Extraction structrec. -Extraction structrec. - -Definition structrec_fun (a : nat) : nat := structrec a (lt_wf a). -Print structrec_fun. diff --git a/plugins/subtac/test/take.v b/plugins/subtac/test/take.v deleted file mode 100644 index 90ae8bae..00000000 --- a/plugins/subtac/test/take.v +++ /dev/null @@ -1,34 +0,0 @@ -(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) -Require Import JMeq. -Require Import List. -Require Import Program. - -Set Implicit Arguments. -Obligations Tactic := idtac. - -Print cons. - -Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } := - match n with - | 0 => nil - | S p => - match l with - | cons hd tl => let rest := take tl p in cons hd rest - | nil => ! - end - end. - -Require Import Omega. -Solve All Obligations. -Next Obligation. - destruct_call take ; program_simpl. -Defined. - -Next Obligation. - intros. - inversion H. -Defined. - - - - diff --git a/plugins/subtac/test/wf.v b/plugins/subtac/test/wf.v deleted file mode 100644 index 5ccc154a..00000000 --- a/plugins/subtac/test/wf.v +++ /dev/null @@ -1,48 +0,0 @@ -Notation "( x & y )" := (@existS _ _ x y) : core_scope. -Unset Printing All. -Require Import Coq.Arith.Compare_dec. - -Require Import Coq.subtac.Utils. - -Ltac one_simpl_hyp := - match goal with - | [H : (`exist _ _ _) = _ |- _] => simpl in H - | [H : _ = (`exist _ _ _) |- _] => simpl in H - | [H : (`exist _ _ _) < _ |- _] => simpl in H - | [H : _ < (`exist _ _ _) |- _] => simpl in H - | [H : (`exist _ _ _) <= _ |- _] => simpl in H - | [H : _ <= (`exist _ _ _) |- _] => simpl in H - | [H : (`exist _ _ _) > _ |- _] => simpl in H - | [H : _ > (`exist _ _ _) |- _] => simpl in H - | [H : (`exist _ _ _) >= _ |- _] => simpl in H - | [H : _ >= (`exist _ _ _) |- _] => simpl in H - end. - -Ltac one_simpl_subtac := - destruct_exists ; - repeat one_simpl_hyp ; simpl. - -Ltac simpl_subtac := do 3 one_simpl_subtac ; simpl. - -Require Import Omega. -Require Import Wf_nat. - -Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt} : - { q : nat & { r : nat | a = b * q + r /\ r < b } } := - if le_lt_dec b a then let (q', r) := euclid (a - b) b in - (S q' & r) - else (O & a). -destruct b ; simpl_subtac. -omega. -simpl_subtac. -assert(x0 * S q' = x0 + x0 * q'). -rewrite <- mult_n_Sm. -omega. -rewrite H2 ; omega. -simpl_subtac. -split ; auto with arith. -omega. -apply lt_wf. -Defined. - -Check euclid_evars_proof.
\ No newline at end of file |