diff options
Diffstat (limited to 'plugins/subtac')
33 files changed, 6689 insertions, 0 deletions
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml new file mode 100644 index 00000000..4b95df19 --- /dev/null +++ b/plugins/subtac/eterm.ml @@ -0,0 +1,233 @@ +(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *) +(** + - 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_loc: Util.loc; + ev_typ: types; + ev_tac: tactic option; + ev_deps: Intset.t } + +(** 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 evar_dependencies evm ev = + let one_step deps = + Intset.fold (fun ev s -> + let evi = Evd.find evm ev in + Intset.union (Evarutil.evars_of_evar_info evi) 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 ev) + +let sort_dependencies evl = + List.stable_sort + (fun (id, ev, deps) (id', ev', deps') -> + if id = id' then 0 + else if Intset.mem id deps' then -1 + else if Intset.mem id' deps then 1 + else Pervasives.compare id id') + evl + +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 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_loc = loc; 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_loc = loc; 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, loc, 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 new file mode 100644 index 00000000..406f9433 --- /dev/null +++ b/plugins/subtac/eterm.mli @@ -0,0 +1,34 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) +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 * loc * 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 new file mode 100644 index 00000000..113b1680 --- /dev/null +++ b/plugins/subtac/g_subtac.ml4 @@ -0,0 +1,177 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) +(*i camlp4use: "pa_extend.cmo" i*) + + +(* + Syntax for the subtac terms and types. + Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *) + +(* $Id$ *) + + +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.e = gec "subtac_gallina_loc" + + let subtac_withtac : Tacexpr.raw_tactic_expr option Gram.Entry.e = gec "subtac_withtac" +end + +open Rawterm +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 Constr.binder 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.binder_let: + [[ "("; 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)] + ] ]; + + Constr.binder: + [ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" -> + ([id],default_binder_kind, mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, c, p)])) + | "("; id=Prim.name; ":"; c=Constr.lconstr; ")" -> + ([id],default_binder_kind, c) + | "("; id=Prim.name; lid=LIST1 Prim.name; ":"; c=Constr.lconstr; ")" -> + (id::lid,default_binder_kind, c) + ] ]; + + 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 "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 "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 -> errorlabstrm "Program" (Cerrors.explain_exn 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 + +VERNAC COMMAND EXTEND Subtac_Show_Solver +| [ "Show" "Obligation" "Tactic" ] -> [ + Pp.msgnl (Pptactic.pr_glob_tactic (Global.env ()) (Subtac_obligations.default_tactic_expr ())) ] +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 new file mode 100644 index 00000000..0eba0f63 --- /dev/null +++ b/plugins/subtac/subtac.ml @@ -0,0 +1,250 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +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 Rawterm +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 (evm = Evd.empty) 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 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 print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () + +let start_proof_and_print env isevars idopt k t hook = + start_proof_com env isevars idopt k t hook; + print_subgoals () + +let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (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) -> + if Lib.is_modtype () then + errorlabstrm "Subtac_command.StartProof" + (str "Proof editing mode not supported in module types"); + 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, b) -> + 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 b) + + | 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, b) -> + if Dumpglob.dump () then + List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l; + ignore(Subtac_command.build_corecursive l b) + + (*| 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 -> + debug 2 (Himsg.explain_pattern_matching_error env exn); + raise e + + | Type_errors.TypeError (env, exn) as e -> + debug 2 (Himsg.explain_type_error env exn); + raise e + + | Pretype_errors.PretypeError (env, exn) as e -> + debug 2 (Himsg.explain_pretype_error env exn); + raise e + + | (Stdpp.Exc_located (loc, Proof_type.LtacLocated (_,e')) | + Stdpp.Exc_located (loc, e') as e) -> + debug 2 (str "Parsing exception: "); + (match e' with + | Type_errors.TypeError (env, exn) -> + debug 2 (Himsg.explain_type_error env exn); + raise e + + | Pretype_errors.PretypeError (env, exn) -> + debug 2 (Himsg.explain_pretype_error env exn); + raise e + + | e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e''); + raise e) + + | e -> + msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e); + raise e diff --git a/plugins/subtac/subtac.mli b/plugins/subtac/subtac.mli new file mode 100644 index 00000000..b51150aa --- /dev/null +++ b/plugins/subtac/subtac.mli @@ -0,0 +1,2 @@ +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 new file mode 100644 index 00000000..e8f4f05f --- /dev/null +++ b/plugins/subtac/subtac_cases.ml @@ -0,0 +1,2027 @@ +(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +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 Rawterm +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 : rawconstr; + } + +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 rawpattern_of_partial_history args2 = function + | Continuation (n, args1, h) -> + let args3 = make_anonymous_patvars (n - (List.length args2)) in + build_rawpattern (List.rev_append args1 (args2@args3)) h + | Result pl -> pl + +and build_rawpattern args = function + | Top -> args + | MakeAlias (AliasLeaf, rh) -> + assert (args = []); + rawpattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh + | MakeAlias (AliasConstructor pci, rh) -> + rawpattern_of_partial_history + [PatCstr (dummy_loc, pci, args, Anonymous)] rh + +let complete_history = rawpattern_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 -> rawconstr -> 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 _ -> 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_rawconstr 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_rawconstr 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 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_rawconstr 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 t = mkRel (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 _ -> 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 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 (Lazy.force eq_ind, [| typ; x ; y |]) +let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |]) +let mk_JMeq typ x typ' y = + mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |]) +let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |]) + +let hole = RHole (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 (lift (n - m) 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, + (RApp (dummy_loc, + (RRef (dummy_loc, Lazy.force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars + | _ -> + match na with + Anonymous -> raise (Invalid_argument "vars_of_ctx") + | Name n -> n, RVar (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 (Lazy.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 ("branch_" ^ (string_of_int !i)) in + let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in + let branch = + let bref = RVar (dummy_loc, branch_name) in + match vars_of_ctx rhs_rels with + [] -> bref + | l -> RApp (dummy_loc, bref, l) + in + let branch = match ineqs with + Some _ -> RApp (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_occ all_occurrences (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, 0, [], [], 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 new file mode 100644 index 00000000..90989d2d --- /dev/null +++ b/plugins/subtac/subtac_cases.mli @@ -0,0 +1,23 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +(*i*) +open Util +open Names +open Term +open Evd +open Environ +open Inductiveops +open Rawterm +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 new file mode 100644 index 00000000..59c877c8 --- /dev/null +++ b/plugins/subtac/subtac_classes.ml @@ -0,0 +1,182 @@ +(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +open Pretyping +open Evd +open Environ +open Term +open Rawterm +open Topconstr +open Names +open Libnames +open Pp +open Vernacexpr +open Constrintern +open Subtac_command +open Typeclasses +open Typeclasses_errors +open Termops +open Decl_kinds +open Entries +open Util + +module SPretyping = Subtac_pretyping.Pretyping + +let interp_constr_evars_gen evdref env ?(impls=([],[])) 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=([],[])) c typ = + interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c + +let interp_context_evars evdref env params = + Constrintern.interp_context_gen + (fun env t -> SPretyping.understand_tcc_evars evdref env IsType t) + (SPretyping.understand_judgment_tcc evdref) !evdref env params + +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 ~onlyargs:true ~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 + let env' = push_rel_context ctx env in + evars := Evarutil.nf_evar_map !evars; + evars := resolve_typeclasses ~onlyargs:false ~fail:true env !evars; + let sigma = !evars in + let subst = List.map (Evarutil.nf_evar sigma) subst in + let props = + match props with + | 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 + | _ -> Inr props + in + let subst = + match props with + | Inr term -> + let c = interp_casted_constr_evars evars env' term cty in + Inr (c, subst) + | 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 + Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid 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; + 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 app (ctx' @ ctx) in + term, termtype + | Inr (def, subst) -> + 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 + let inst = Typeclasses.new_instance k pri global (ConstRef cst) in + Impargs.declare_manual_implicits false gr ~enriching:false imps; + Typeclasses.add_instance inst + 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,false,Instance) ~hook obls diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli new file mode 100644 index 00000000..ee78ff68 --- /dev/null +++ b/plugins/subtac/subtac_classes.mli @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +(*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 -> + ?generalize:bool -> + int option -> + identifier * Subtac_obligations.progress diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml new file mode 100644 index 00000000..5337baca --- /dev/null +++ b/plugins/subtac/subtac_coercion.ml @@ -0,0 +1,503 @@ +(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* $Id$ *) + +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 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_ = Lazy.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 (Lazy.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 (Lazy.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 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 isevars = ref isevars in + 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 + (Some (fun x -> + app_opt f (mkApp ((Lazy.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 x = nf_evar ( !isevars) x and y = nf_evar ( !isevars) y in + 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 :: lift_args 1 tele) in + let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in + let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in + let evar = make_existential loc env isevars eq in + let eq_app x = mkApp (Lazy.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 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 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 = Lazy.force existS in + let prod = Lazy.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 !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 c1 (mkApp (existS.proj1, + [| a; pb; x |])), + app_opt 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 c1 (mkApp (prod.proj1, + [| a; b; x |])), + app_opt 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 c (mkApp ((Lazy.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 c x in + let evar = make_existential loc env isevars (mkApp (p, [| cx |])) + in + (mkApp + ((Lazy.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 + !evars, Option.map (app_opt coercion) v + + (* 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 Rawterm.PatVar (loc, Anonymous) else pat in + Rawterm.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 _ -> anomaly "apply_coercion" + + let inh_app_fun env isevars j = + let t = whd_betadeltaiota 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 + (isevars, { uj_val = app_opt coercef j.uj_val; uj_type = t }) + 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 = whd_betadeltaiota 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 typ = whd_betadeltaiota env ( isevars) j.uj_type in + let ct, typ' = mu env isevars typ in + isevars, { uj_val = app_opt ct j.uj_val; + uj_type = typ' } + + let inh_coerce_to_prod loc env isevars t = + let typ = whd_betadeltaiota 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 (evd', val') = + try + inh_conv_coerce_to_fail loc env evd rigidonly + (Some (nf_evar evd cj.uj_val)) + (nf_evar evd cj.uj_type) (nf_evar evd t) + with NoCoercion -> + let sigma = evd in + try + coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t + with NoSubtacCoercion -> + error_actual_type_loc loc env sigma 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 -> + let sigma = isevars in + error_cannot_coerce env' sigma (t, t')) + else isevars + with _ -> isevars +end diff --git a/plugins/subtac/subtac_coercion.mli b/plugins/subtac/subtac_coercion.mli new file mode 100644 index 00000000..5678c10e --- /dev/null +++ b/plugins/subtac/subtac_coercion.mli @@ -0,0 +1,4 @@ +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 new file mode 100644 index 00000000..f2747225 --- /dev/null +++ b/plugins/subtac/subtac_command.ml @@ -0,0 +1,534 @@ +open Closure +open RedFlags +open Declarations +open Entries +open Libobject +open Pattern +open Matching +open Pp +open Rawterm +open Sign +open Tacred +open Util +open Names +open Nameops +open Libnames +open Nametab +open Pfedit +open Proof_type +open Refiner +open Tacmach +open Tactic_debug +open Topconstr +open Term +open Termops +open Tacexpr +open Safe_typing +open Typing +open Hiddentac +open Genarg +open Decl_kinds +open Mod_subst +open Printer +open Inductiveops +open Syntax_def +open Environ +open Tactics +open Tacticals +open Tacinterp +open Vernacexpr +open Notation +open Evd +open Evarutil + +module SPretyping = Subtac_pretyping.Pretyping +open Subtac_utils +open Pretyping +open Subtac_obligations + +(*********************************************************************) +(* Functions to parse and interpret constructions *) + +let evar_nf isevars c = + Evarutil.nf_evar !isevars c + +let interp_gen kind isevars env + ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) + c = + let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in + let c' = SPretyping.understand_tcc_evars isevars env kind c' in + evar_nf isevars c' + +let interp_constr isevars env c = + interp_gen (OfType None) isevars env c + +let interp_type_evars isevars env ?(impls=([],[])) c = + interp_gen IsType isevars env ~impls c + +let interp_casted_constr isevars env ?(impls=([],[])) c typ = + interp_gen (OfType (Some typ)) isevars env ~impls c + +let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ = + interp_gen (OfType (Some typ)) isevars env ~impls c + +let interp_open_constr isevars env c = + msgnl (str "Pretyping " ++ my_print_constr_expr c); + let c = Constrintern.intern_constr ( !isevars) env c in + let c' = SPretyping.understand_tcc_evars isevars env (OfType None) c in + evar_nf isevars c' + +let interp_constr_judgment isevars env c = + let j = + SPretyping.understand_judgment_tcc isevars env + (Constrintern.intern_constr ( !isevars) env c) + in + { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type } + +let locate_if_isevar loc na = function + | RHole _ -> + (try match na with + | Name id -> Reserve.find_reserved_type id + | Anonymous -> raise Not_found + with Not_found -> RHole (loc, Evd.BinderType na)) + | x -> x + +let interp_binder sigma env na t = + let t = Constrintern.intern_gen true ( !sigma) env t in + SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_rawconstr t) na t) + +let interp_context_evars evdref env params = + let bl = Constrintern.intern_context false ( !evdref) env params in + let (env, par, _, impls) = + List.fold_left + (fun (env,params,n,impls) (na, k, b, t) -> + match b with + None -> + let t' = locate_if_isevar (loc_of_rawconstr t) na t in + let t = SPretyping.understand_tcc_evars evdref env IsType t' in + let d = (na,None,t) in + let impls = + if k = Implicit then + let na = match na with Name n -> Some n | Anonymous -> None in + (ExplByPos (n, na), (true, true, true)) :: impls + else impls + in + (push_rel d env, d::params, succ n, impls) + | Some b -> + let c = SPretyping.understand_judgment_tcc evdref env b in + let d = (na, Some c.uj_val, c.uj_type) in + (push_rel d env,d::params, succ n, impls)) + (env,[],1,[]) (List.rev bl) + in (env, par), impls + +(* try to find non recursive definitions *) + +let list_chop_hd i l = match list_chop i l with + | (l1,x::l2) -> (l1,x,l2) + | (x :: [], l2) -> ([], x, []) + | _ -> assert(false) + +let collect_non_rec env = + let rec searchrec lnonrec lnamerec ldefrec larrec nrec = + try + let i = + list_try_find_i + (fun i f -> + if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec + then i else failwith "try_find_i") + 0 lnamerec + in + let (lf1,f,lf2) = list_chop_hd i lnamerec in + let (ldef1,def,ldef2) = list_chop_hd i ldefrec in + let (lar1,ar,lar2) = list_chop_hd i larrec in + let newlnv = + try + match list_chop i nrec with + | (lnv1,_::lnv2) -> (lnv1@lnv2) + | _ -> [] (* nrec=[] for cofixpoints *) + with Failure "list_chop" -> [] + in + searchrec ((f,def,ar)::lnonrec) + (lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv + with Failure "try_find_i" -> + (List.rev lnonrec, + (Array.of_list lnamerec, Array.of_list ldefrec, + Array.of_list larrec, Array.of_list nrec)) + in + searchrec [] + +let list_of_local_binders l = + let rec aux acc = function + Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl + | Topconstr.LocalRawAssum (nl, k, c) :: tl -> + aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl + | [] -> List.rev acc + in aux [] l + +let lift_binders k n l = + let rec aux n = function + | (id, t, c) :: tl -> (id, Option.map (liftn k n) t, liftn k n c) :: aux (pred n) tl + | [] -> [] + in aux n l + +let rec gen_rels = function + 0 -> [] + | n -> mkRel n :: gen_rels (pred n) + +let split_args n rel = match list_chop ((List.length rel) - n) rel with + (l1, x :: l2) -> l1, x, l2 + | _ -> assert(false) + +open Coqlib + +let sigT = Lazy.lazy_from_fun build_sigma_type +let sigT_info = lazy + { ci_ind = destInd (Lazy.force sigT).typ; + ci_npar = 2; + ci_cstr_nargs = [|2|]; + ci_pp_info = { ind_nargs = 0; style = LetStyle } + } + +let telescope = function + | [] -> assert false + | [(n, None, t)] -> t, [n, Some (mkRel 1), t], mkRel 1 + | (n, None, t) :: tl -> + let ty, tys, (k, constr) = + List.fold_left + (fun (ty, tys, (k, constr)) (n, b, t) -> + let pred = mkLambda (n, t, ty) in + let sigty = mkApp ((Lazy.force sigT).typ, [|t; pred|]) in + let intro = mkApp ((Lazy.force sigT).intro, [|lift k t; lift k pred; mkRel k; constr|]) in + (sigty, pred :: tys, (succ k, intro))) + (t, [], (2, mkRel 1)) tl + in + let (last, subst) = List.fold_right2 + (fun pred (n, b, t) (prev, subst) -> + let proj1 = applistc (Lazy.force sigT).proj1 [t; pred; prev] in + let proj2 = applistc (Lazy.force sigT).proj2 [t; pred; prev] in + (lift 1 proj2, (n, Some proj1, t) :: subst)) + (List.rev tys) tl (mkRel 1, []) + in ty, ((n, Some last, t) :: subst), constr + + | _ -> raise (Invalid_argument "telescope") + +let nf_evar_context isevars ctx = + List.map (fun (n, b, t) -> + (n, Option.map (Evarutil.nf_evar isevars) b, Evarutil.nf_evar isevars t)) ctx + +let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = + Coqlib.check_required_library ["Coq";"Program";"Wf"]; + let sigma = Evd.empty in + let isevars = ref (Evd.create_evar_defs sigma) in + let env = Global.env() in + let _pr c = my_print_constr env c in + let _prr = Printer.pr_rel_context env in + let _prn = Printer.pr_named_context env in + let _pr_rel env = Printer.pr_rel_context env in + let (env', binders_rel), impls = interp_context_evars isevars env bl in + let len = List.length binders_rel in + let top_env = push_rel_context binders_rel env in + let top_arity = interp_type_evars isevars top_env arityc in + let full_arity = it_mkProd_or_LetIn top_arity binders_rel in + let argtyp, letbinders, make = telescope binders_rel in + let argname = id_of_string "recarg" in + let arg = (Name argname, None, argtyp) in + let binders = letbinders @ [arg] in + let binders_env = push_rel_context binders_rel env in + let rel = interp_constr isevars env r in + let relty = type_of env !isevars rel in + let relargty = + let ctx, ar = Reductionops.splay_prod_n env !isevars 2 relty in + match ctx, kind_of_term ar with + | [(_, None, t); (_, None, u)], Sort (Prop Null) + when Reductionops.is_conv env !isevars t u -> t + | _, _ -> + user_err_loc (constr_loc r, + "Subtac_command.build_wellfounded", + my_print_constr env rel ++ str " is not an homogeneous binary relation.") + in + let measure = interp_casted_constr isevars binders_env measure relargty in + let wf_rel, wf_rel_fun, measure_fn = + let measure_body, measure = + it_mkLambda_or_LetIn measure letbinders, + it_mkLambda_or_LetIn measure binders + in + let comb = constr_of_global (Lazy.force measure_on_R_ref) in + let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in + let wf_rel_fun x y = + mkApp (rel, [| subst1 x measure_body; + subst1 y measure_body |]) + in wf_rel, wf_rel_fun, measure + in + let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |]) in + let argid' = id_of_string (string_of_id argname ^ "'") in + let wfarg len = (Name argid', None, + mkSubset (Name argid') argtyp + (wf_rel_fun (mkRel 1) (mkRel (len + 1)))) + in + let intern_bl = wfarg 1 :: [arg] in + let _intern_env = push_rel_context intern_bl env in + let proj = (Lazy.force sig_).Coqlib.proj1 in + let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in + let projection = (* in wfarg :: arg :: before *) + mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |]) + in + let top_arity_let = it_mkLambda_or_LetIn top_arity letbinders in + let intern_arity = substl [projection] top_arity_let in + (* substitute the projection of wfarg for something, + now intern_arity is in wfarg :: arg *) + let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in + let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in + let curry_fun = + let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in + let arg = mkApp ((Lazy.force sig_).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in + let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in + let rcurry = mkApp (rel, [| measure; lift len measure |]) in + let lam = (Name (id_of_string "recproof"), None, rcurry) in + let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in + let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in + (Name recname, Some body, ty) + in + let fun_bl = intern_fun_binder :: [arg] in + let lift_lets = Termops.lift_rel_context 1 letbinders in + let intern_body = + let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in + let (r, l, impls, scopes) = + Constrintern.compute_internalization_data env + Constrintern.Recursive full_arity impls + in + let newimpls = [(recname, (r, l, impls @ + [Some (id_of_string "recproof", Impargs.Manual, (true, false))], + scopes @ [None]))] in + let newimpls = Constrintern.set_internalization_env_params newimpls [] in + interp_casted_constr isevars ~impls:newimpls + (push_rel_context ctx env) body (lift 1 top_arity) + in + let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in + let prop = mkLambda (Name argname, argtyp, top_arity_let) in + let def = + mkApp (constr_of_global (Lazy.force fix_sub_ref), + [| argtyp ; wf_rel ; + make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ; + prop ; intern_body_lam |]) + in + let _ = isevars := Evarutil.nf_evar_map !isevars in + let binders_rel = nf_evar_context !isevars binders_rel in + let binders = nf_evar_context !isevars binders in + let top_arity = Evarutil.nf_evar !isevars top_arity in + let hook, recname, typ = + if List.length binders_rel > 1 then + let name = add_suffix recname "_func" in + let hook l gr = + let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in + let ty = it_mkProd_or_LetIn top_arity binders_rel in + let ce = + { const_entry_body = Evarutil.nf_evar !isevars body; + const_entry_type = Some ty; + const_entry_opaque = false; + const_entry_boxed = false} + in + let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in + let gr = ConstRef c in + if Impargs.is_implicit_args () || impls <> [] then + Impargs.declare_manual_implicits false gr impls + in + let typ = it_mkProd_or_LetIn top_arity binders in + hook, name, typ + else + let typ = it_mkProd_or_LetIn top_arity binders_rel in + let hook l gr = + if Impargs.is_implicit_args () || impls <> [] then + Impargs.declare_manual_implicits false gr impls + in hook, recname, typ + in + let fullcoqc = Evarutil.nf_evar !isevars def in + let fullctyp = Evarutil.nf_evar !isevars typ in + let evm = evars_of_term !isevars Evd.empty fullctyp in + let evm = evars_of_term !isevars evm fullcoqc in + let evm = non_instanciated_map env isevars evm in + let evars, _, evars_def, evars_typ = + Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp + in + Subtac_obligations.add_definition recname ~term:evars_def evars_typ evars ~hook + +let interp_fix_context evdref env fix = + interp_context_evars evdref env fix.Command.fix_binders + +let interp_fix_ccl evdref (env,_) fix = + interp_type_evars evdref env fix.Command.fix_type + +let interp_fix_body evdref env_rec impls (_,ctx) fix ccl = + let env = push_rel_context ctx env_rec in + let body = Option.map (fun c -> interp_casted_constr_evars evdref env ~impls c ccl) fix.Command.fix_body in + Option.map (fun c -> it_mkLambda_or_LetIn c ctx) body + +let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx + +let prepare_recursive_declaration fixnames fixtypes fixdefs = + let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in + let names = List.map (fun id -> Name id) fixnames in + (Array.of_list names, Array.of_list fixtypes, Array.of_list defs) + +let rel_index n ctx = + list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx)) + +let rec unfold f b = + match f b with + | Some (x, b') -> x :: unfold f b' + | None -> [] + +let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype = + match n with + | Some (loc, n) -> [rel_index n fixctx] + | None -> + (* If recursive argument was not given by user, we try all args. + An earlier approach was to look only for inductive arguments, + but doing it properly involves delta-reduction, and it finally + doesn't seem to worth the effort (except for huge mutual + fixpoints ?) *) + let len = List.length fixctx in + unfold (function x when x = len -> None + | n -> Some (n, succ n)) 0 + +let push_named_context = List.fold_right push_named + +let check_evars env initial_sigma evd c = + let sigma = evd in + let c = nf_evar sigma c in + let rec proc_rec c = + match kind_of_term c with + | Evar (evk,args) -> + assert (Evd.mem sigma evk); + if not (Evd.mem initial_sigma evk) then + let (loc,k) = evar_source evk evd in + (match k with + | QuestionMark _ + | ImplicitArg (_, _, false) -> () + | _ -> + let evi = nf_evar_info sigma (Evd.find sigma evk) in + Pretype_errors.error_unsolvable_implicit loc env sigma evi k None) + | _ -> iter_constr proc_rec c + in proc_rec c + +let out_def = function + | Some def -> def + | None -> error "Program Fixpoint needs defined bodies." + +let interp_recursive fixkind l boxed = + let env = Global.env() in + let fixl, ntnl = List.split l in + let kind = fixkind <> IsCoFixpoint in + let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in + + (* Interp arities allowing for unresolved types *) + let evdref = ref Evd.empty in + let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in + let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in + let fixtypes = List.map2 build_fix_type fixctxs fixccls in + let rec_sign = + List.fold_left2 (fun env' id t -> + let sort = Retyping.get_type_of env !evdref t in + let fixprot = + try mkApp (Lazy.force Subtac_utils.fix_proto, [|sort; t|]) + with e -> t + in + (id,None,fixprot) :: env') + [] fixnames fixtypes + in + let env_rec = push_named_context rec_sign env in + + (* Get interpretation metadatas *) + let impls = Constrintern.compute_full_internalization_env env + Constrintern.Recursive [] fixnames fixtypes fiximps + in + let notations = List.flatten ntnl in + + (* Interp bodies with rollback because temp use of notations/implicit *) + let fixdefs = + States.with_state_protection (fun () -> + List.iter (Metasyntax.set_notation_for_interpretation impls) notations; + list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls) + () in + + let fixdefs = List.map out_def fixdefs in + + (* Instantiate evars and check all are resolved *) + let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in + let evd = Typeclasses.resolve_typeclasses + ~onlyargs:true ~split:true ~fail:false env_rec evd + in + let evd = Evarutil.nf_evar_map evd in + let fixdefs = List.map (nf_evar evd) fixdefs in + let fixtypes = List.map (nf_evar evd) fixtypes in + let rec_sign = nf_named_context_evar evd rec_sign in + + let recdefs = List.length rec_sign in + List.iter (check_evars env_rec Evd.empty evd) fixdefs; + List.iter (check_evars env Evd.empty evd) fixtypes; + Command.check_mutuality env kind (List.combine fixnames fixdefs); + + (* Russell-specific code *) + + (* Get the interesting evars, those that were not instanciated *) + let isevars = Evd.undefined_evars evd in + let evm = isevars in + (* Solve remaining evars *) + let rec collect_evars id def typ imps = + (* Generalize by the recursive prototypes *) + let def = + Termops.it_mkNamedLambda_or_LetIn def rec_sign + and typ = + Termops.it_mkNamedProd_or_LetIn typ rec_sign + in + let evm' = Subtac_utils.evars_of_term evm Evd.empty def in + let evm' = Subtac_utils.evars_of_term evm evm' typ in + let evars, _, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in + (id, def, typ, imps, evars) + in + let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in + (match fixkind with + | IsFixpoint wfl -> + let possible_indexes = + list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in + let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), + Array.of_list fixtypes, + Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) + in + let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in + list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) l + | IsCoFixpoint -> ()); + Subtac_obligations.add_mutual_definitions defs notations fixkind + +let out_n = function + Some n -> n + | None -> raise Not_found + +let build_recursive l b = + let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in + match g, l with + [(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] -> + ignore(build_wellfounded (id, n, bl, typ, out_def def) r + (match n with Some n -> mkIdentC (snd n) | None -> + errorlabstrm "Subtac_command.build_recursive" + (str "Recursive argument required for well-founded fixpoints")) + ntn false) + + | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] -> + ignore(build_wellfounded (id, n, bl, typ, out_def def) (Option.default (CRef lt_ref) r) + m ntn false) + + | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g -> + let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) -> + ({Command.fix_name = id; Command.fix_binders = bl; + Command.fix_body = def; Command.fix_type = typ},ntn)) l + in interp_recursive (IsFixpoint g) fixl b + | _, _ -> + errorlabstrm "Subtac_command.build_recursive" + (str "Well-founded fixpoints not allowed in mutually recursive blocks") + +let build_corecursive l b = + let fixl = List.map (fun (((_,id),bl,typ,def),ntn) -> + ({Command.fix_name = id; Command.fix_binders = bl; + Command.fix_body = def; Command.fix_type = typ},ntn)) + l in + interp_recursive IsCoFixpoint fixl b diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli new file mode 100644 index 00000000..304aa139 --- /dev/null +++ b/plugins/subtac/subtac_command.mli @@ -0,0 +1,60 @@ +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:full_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:full_internalization_env -> + constr_expr -> constr +val interp_casted_constr_evars : + evar_map ref -> + env -> + ?impls:full_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 * 'a 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 -> 'c -> Subtac_obligations.progress + +val build_recursive : + (fixpoint_expr * decl_notation list) list -> bool -> unit + +val build_corecursive : + (cofixpoint_expr * decl_notation list) list -> bool -> unit diff --git a/plugins/subtac/subtac_errors.ml b/plugins/subtac/subtac_errors.ml new file mode 100644 index 00000000..067da150 --- /dev/null +++ b/plugins/subtac/subtac_errors.ml @@ -0,0 +1,24 @@ +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 new file mode 100644 index 00000000..8d75b9c0 --- /dev/null +++ b/plugins/subtac/subtac_errors.mli @@ -0,0 +1,15 @@ +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 new file mode 100644 index 00000000..2836bc73 --- /dev/null +++ b/plugins/subtac/subtac_obligations.ml @@ -0,0 +1,652 @@ +(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *) +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 + +let ppwarn cmd = Pp.warn (str"Program:" ++ cmd) +let pperror cmd = Util.errorlabstrm "Program" cmd +let error s = pperror (str s) + +let reduce = + Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty + +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 * loc * obligation_definition_status * Intset.t + * tactic option) array + +type obligation = + { obl_name : identifier; + obl_type : types; + obl_location : loc; + 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_hook : Tacexpr.declaration_hook; +} + +let assumption_message id = + Flags.if_verbose message ((string_of_id id) ^ " is assumed") + +let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC +let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Tacexpr.TacId []) + +let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t + +(* 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; + optname = "transparency of Program obligations"; + optkey = ["Transparent";"Obligations"]; + optread = get_proofs_transparency; + optwrite = set_proofs_transparency; } + +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 subst_deps expand obls deps t = + let subst = + Intset.fold + (fun x acc -> + let xobl = obls.(x) in + let oblb = + try get_obligation_body expand xobl + with _ -> assert(false) + in (xobl.obl_name, oblb) :: acc) + deps [] + in(* Termops.it_mkNamedProd_or_LetIn t subst *) + Term.replace_vars subst t + +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, !default_tactic_expr +let unfreeze (v, t) = from_prg := v; set_default_tactic t +let init () = + from_prg := ProgMap.empty; set_default_tactic (Tacexpr.TacId []) + +(** 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 cache (_, (local, tac)) = + set_default_tactic tac + +let load (_, (local, tac)) = + if not local then set_default_tactic tac + +let subst (s, (local, tac)) = + (local, Tacinterp.subst_tactic s tac) + +let (input,output) = + declare_object + { (default_object "Program state") with + cache_function = cache; + load_function = (fun _ -> load); + open_function = (fun _ -> load); + classify_function = (fun (local, tac) -> + if not (ProgMap.is_empty !from_prg) then + errorlabstrm "Program" (str "Unsolved obligations when closing module:" ++ spc () ++ + prlist_with_sep spc (fun x -> Nameops.pr_id x) + (map_keys !from_prg)); + if local then Dispose else Substitute (local, tac)); + subst_function = subst} + +let update_state local = + Lib.add_anonymous_leaf (input (local, !default_tactic_expr)) + +let set_default_tactic local t = + set_default_tactic t; update_state local + +open Evd + +let progmap_remove prg = + from_prg := ProgMap.remove prg.prg_name !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_deps expand obls ints prg.prg_body, + subst_deps expand obls ints (Termops.refresh_universes prg.prg_type) + +let declare_definition prg = + let body, typ = subst_body true prg in + (try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++ + my_print_constr (Global.env()) body ++ str " : " ++ + my_print_constr (Global.env()) prg.prg_type); + with _ -> ()); + let (local, boxed, kind) = prg.prg_kind in + let ce = + { const_entry_body = body; + const_entry_type = Some typ; + const_entry_opaque = false; + const_entry_boxed = boxed} + 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 (pi3 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 + reduce term, 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,boxed,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 boxed 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 = reduce body in + let ty = 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_type = Some ty; + const_entry_opaque = opaque; + const_entry_boxed = false} + 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 red = Reductionops.nf_betaiota Evd.empty + +let init_prog_info n b t deps fixkind notations obls impls kind 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; 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 = red t; obl_status = o; + obl_deps = d; obl_tac = tac }) + obls, b + in + { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls'); + prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; + prg_implicits = impls; prg_kind = kind; 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 + from_prg := map_replace prg.prg_name prg' !from_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 has_dependencies obls n = + let res = ref false in + Array.iteri + (fun i obl -> + if i <> n && Intset.mem n obl.obl_deps then + res := true) + 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 -> pperror (Cerrors.explain_exn e) + in + match res with + | Remain n when n > 0 -> + if has_dependencies obls num then + ignore(auto_solve_obligations (Some prg.prg_name) None) + | _ -> ()); + trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ + Subtac_utils.my_print_constr (Global.env ()) obl.obl_type); + Pfedit.by !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 -> !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 + | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s))) + | Stdpp.Exc_located(_, Refiner.FailError (_, s)) + | Refiner.FailError (_, s) -> + user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s) + | e -> false + +and solve_prg_obligations prg tac = + let obls, rem = prg.prg_obligations in + let rem = ref rem in + let obls' = Array.copy obls in + let _ = + Array.iteri (fun i x -> + if solve_obligation_by_tac prg obls' i tac then + 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 tac : progress = + Flags.if_verbose msgnl (str "Solving obligations automatically..."); + try solve_prg_obligations (get_prog_err n) 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,false,Definition) ?tactic ?(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 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 + from_prg := ProgMap.add n prg !from_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,false,Definition) ?(hook=fun _ _ -> ()) notations fixkind = + let deps = List.map (fun (n, b, t, imps, obls) -> n) l in + let upd = List.fold_left + (fun acc (n, b, t, imps, obls) -> + let prg = init_prog_info n (Some b) t deps (Some fixkind) notations obls imps kind hook in + ProgMap.add n prg acc) + !from_prg l + in + from_prg := upd; + 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 + 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 (x.obl_type,false), + 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 + +let default_tactic () = !default_tactic +let default_tactic_expr () = !default_tactic_expr diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli new file mode 100644 index 00000000..1608c134 --- /dev/null +++ b/plugins/subtac/subtac_obligations.mli @@ -0,0 +1,69 @@ +open Names +open Util +open Libnames +open Evd +open Proof_type + +type obligation_info = + (identifier * Term.types * loc * + 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 default_tactic : unit -> Proof_type.tactic +val default_tactic_expr : unit -> Tacexpr.glob_tactic_expr + +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 -> + ?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 -> + ?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 new file mode 100644 index 00000000..a4b9d67e --- /dev/null +++ b/plugins/subtac/subtac_plugin.mllib @@ -0,0 +1,13 @@ +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 new file mode 100644 index 00000000..f1541f25 --- /dev/null +++ b/plugins/subtac/subtac_pretyping.ml @@ -0,0 +1,137 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +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 Rawterm +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_rawconstr env c) ++ *) +(* str " and tycon "++ my_print_tycon env tycon ++ *) +(* str " in environment: " ++ my_print_env env); *) + +let merge_evms x y = + Evd.fold (fun ev evi evm -> Evd.add evm ev evi) x y + +let interp env isevars c tycon = + let j = pretype 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 ~onlyargs:true ~split:true ~fail:true env evd in + let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:false ~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 -> Rawterm.rawconstr = Constrintern.intern_constr ( evd) env +let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = 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 env isevars id bl c tycon = + let c = Topconstr.abstract_constr_expr c bl in + let tycon = + match tycon with + None -> empty_tycon + | Some t -> + let t = Topconstr.prod_constr_expr t bl in + let t = coqintern_type !isevars env t in + let coqt, ttyp = interp env isevars t empty_tycon in + mk_tycon coqt + in + let c = coqintern_constr !isevars env c in + let imps = Implicit_quantifiers.implicits_of_rawterm 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 new file mode 100644 index 00000000..055c6df2 --- /dev/null +++ b/plugins/subtac/subtac_pretyping.mli @@ -0,0 +1,23 @@ +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 -> + Rawterm.rawconstr -> + Evarutil.type_constraint -> Term.constr * Term.constr + +val subtac_process : 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 new file mode 100644 index 00000000..e574ef3b --- /dev/null +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -0,0 +1,645 @@ +(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +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 Nameops +open Classops +open List +open Recordops +open Evarutil +open Pretype_errors +open Rawterm +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 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 i lft.(i) explft.(i) + done + + (* coerce to tycon if any *) + let inh_conv_coerce_to_tycon loc env evdref j = function + | None -> j_nf_evar !evdref j + | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to 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 (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 (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) = 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=it_mkLambda ccl' sign; uj_type=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 = function + | RProp c -> judge_of_prop_contents c + | RType _ -> judge_of_new_Type () + + (* [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 (tycon : type_constraint) env evdref lvar c = +(* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_rawconstr env c ++ *) +(* str " with tycon " ++ Evarutil.pr_tycon env tycon) *) +(* with _ -> () *) +(* in *) + match c with + | RRef (loc,ref) -> + inh_conv_coerce_to_tycon loc env evdref + (pretype_ref evdref env ref) + tycon + + | RVar (loc, id) -> + inh_conv_coerce_to_tycon loc env evdref + (pretype_id loc env !evdref lvar id) + tycon + + | REvar (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 + + | RPatVar (loc,(someta,n)) -> + anomaly "Found a pattern variable in a rawterm to type" + + | RHole (loc,k) -> + let ty = + match tycon with + | Some (None, ty) -> ty + | None | Some _ -> + e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in + { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty } + + | RRec (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 (Lazy.force Subtac_utils.fix_proto, [| sort; ty |])) + ftys + in + push_rec_types (names,marked_ftys,[||]) env + in + let fixi = match fixkind with RFix (vn, i) -> i | RCoFix 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 + | RFix (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) + | RCoFix i -> + let cofix = (i,(names,ftys,fdefs)) in + (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e); + make_judge (mkCoFix cofix) ftys.(i) in + inh_conv_coerce_to_tycon loc env evdref fixj tycon + + | RSort (loc,s) -> + inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon + + | RApp (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) when Subtac_coercion.disc_subset t = None -> ty + | _ -> None + in + let fj = pretype ftycon env evdref lvar f in + let floc = loc_of_rawconstr f in + let rec apply_rec env n resj tycon = function + | [] -> resj + | c::rest -> + let argloc = loc_of_rawconstr c in + let resj = evd_comb1 (Coercion.inh_app_fun 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 (nf_evar !evdref c1)) env evdref lvar c in + let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in + let typ' = nf_evar !evdref typ in + apply_rec env (n+1) + { uj_val = nf_evar !evdref value; + uj_type = nf_evar !evdref typ' } + (Option.map (fun (abs, c) -> abs, nf_evar !evdref 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 = j_nf_evar ( !evdref) (apply_rec env 1 fj ftycon args) in + let resj = + match kind_of_term 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 + + | RLambda(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 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 + + | RProd(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' = 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 -> Stdpp.raise_with_loc loc e in + inh_conv_coerce_to_tycon loc env evdref resj tycon + + | RLetIn(loc,name,c1,c2) -> + let j = pretype empty_tycon env evdref lvar c1 in + let t = 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 } + + | RLetTuple (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_rawconstr 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 }) + + | RIf (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_rawconstr 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) (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 + (* msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*) + let f cs b = + let n = rel_context_length cs.cs_args in + let pi = lift n pred in (* liftn n 2 pred ? *) + 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 +(* msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *) + 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 } + + | RCases (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) + + | RCast (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 + (* User Casts are for helping pretyping, experimentally not to be kept*) + (* ... except for Correctness *) + 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 + + | RDynamic (loc,d) -> + if (Dyn.tag d) = "constr" then + let c = constr_out d in + let j = (Retyping.get_judgment_of env ( !evdref) c) in + j + (*inh_conv_coerce_to_tycon loc env evdref j tycon*) + else + user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic.")) + + (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) + and pretype_type valcon env evdref lvar = function + | RHole 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 = new_Type_sort () in + { utj_val = e_new_evar evdref env ~src:loc (mkSort s); + utj_type = s}) + | c -> + let j = pretype empty_tycon env evdref lvar c in + let loc = loc_of_rawconstr 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_rawconstr 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 tycon env evdref lvar c).uj_val + | IsType -> + (pretype_type empty_valcon env evdref lvar c).utj_val in + evdref := fst (consider_remaining_unif_problems env !evdref); + if resolve_classes then + evdref := + Typeclasses.resolve_typeclasses ~onlyargs:false + ~split:true ~fail:fail_evar 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 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 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 expand_evar sigma env lvar kind c = + ise_pretype_gen expand_evar false true 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 new file mode 100644 index 00000000..06a80f68 --- /dev/null +++ b/plugins/subtac/subtac_utils.ml @@ -0,0 +1,484 @@ +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 fix_sub_module = "Wf" +let utils_module = "Utils" +let fixsub_module = subtac_dir @ [fix_sub_module] +let utils_module = subtac_dir @ [utils_module] +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 fixsub = lazy (init_constant fixsub_module "Fix_sub") +let ex_pi1 = lazy (init_constant utils_module "ex_pi1") +let ex_pi2 = lazy (init_constant utils_module "ex_pi2") + +let make_ref l s = lazy (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_ = lazy (build_sig ()) + +let fix_proto = lazy (init_constant tactics_module "fix_proto") +let fix_proto_ref () = + match Nametab.global (make_ref "Program.Tactics.fix_proto") with + | ConstRef c -> c + | _ -> assert false + +let eq_ind = lazy (init_constant ["Init"; "Logic"] "eq") +let eq_rec = lazy (init_constant ["Init"; "Logic"] "eq_rec") +let eq_rect = lazy (init_constant ["Init"; "Logic"] "eq_rect") +let eq_refl = lazy (init_constant ["Init"; "Logic"] "refl_equal") +let eq_ind_ref = lazy (init_reference ["Init"; "Logic"] "eq") +let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal") + +let not_ref = lazy (init_constant ["Init"; "Logic"] "not") + +let and_typ = lazy (Coqlib.build_coq_and ()) + +let eqdep_ind = lazy (init_constant [ "Logic";"Eqdep"] "eq_dep") +let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec") +let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep") +let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro") + +let jmeq_ind = + lazy (check_required_library ["Coq";"Logic";"JMeq"]; + init_constant ["Logic";"JMeq"] "JMeq") +let jmeq_rec = + lazy (check_required_library ["Coq";"Logic";"JMeq"]; + init_constant ["Logic";"JMeq"] "JMeq_rec") +let jmeq_refl = + lazy (check_required_library ["Coq";"Logic";"JMeq"]; + init_constant ["Logic";"JMeq"] "JMeq_refl") + +let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex") +let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro") + +let proj1 = lazy (init_constant ["Init"; "Logic"] "proj1") +let proj2 = lazy (init_constant ["Init"; "Logic"] "proj2") + +let boolind = lazy (init_constant ["Init"; "Datatypes"] "bool") +let sumboolind = lazy (init_constant ["Init"; "Specif"] "sumbool") +let natind = lazy (init_constant ["Init"; "Datatypes"] "nat") +let intind = lazy (init_constant ["ZArith"; "binint"] "Z") +let existSind = lazy (init_constant ["Init"; "Specif"] "sigS") + +let existS = lazy (build_sigma_type ()) + +let prod = lazy (build_prod ()) + + +(* orders *) +let well_founded = lazy (init_constant ["Init"; "Wf"] "well_founded") +let fix = lazy (init_constant ["Init"; "Wf"] "Fix") +let acc = lazy (init_constant ["Init"; "Wf"] "Acc") +let acc_inv = lazy (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_rawconstr = Printer.pr_rawconstr_env +let my_print_evardefs = Evd.pr_evar_map + +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") + (lazy (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 = + let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in + let (key, args) = destEvar evar in + (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++ + print_args env args ++ str " for type: "++ + my_print_constr env c) with _ -> ()); + evar + +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 id x = x +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 _ -> ()); + let tac = assert_tac (Name n) hyptype in + let conttac = + (fun cont -> + conttac + (tclTHENS tac + ([intros; + (tclTHENSEQ + [constructor_tac false (Some 1) 1 + (Rawterm.ImplicitBindings [mkVar n]); + cont]); + ]))) + in + let conttype = + (fun typ -> + let tex = mkLambda (Name n, t, typ) in + conttype + (mkApp (Lazy.force 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 [] id id (List.rev l) + +open Proof_type +open Tacexpr + +let mkProj1 a b c = + mkApp (Lazy.force proj1, [| a; b; c |]) + +let mkProj2 a b c = + mkApp (Lazy.force proj2, [| a; b; c |]) + +let mk_ex_pi1 a b c = + mkApp (Lazy.force ex_pi1, [| a; b; c |]) + +let mk_ex_pi2 a b c = + mkApp (Lazy.force ex_pi2, [| a; b; c |]) + +let mkSubset name typ prop = + mkApp ((Lazy.force sig_).typ, + [| typ; mkLambda (name, typ, prop) |]) + +let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |]) +let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |]) +let mk_JMeq typ x typ' y = mkApp (Lazy.force jmeq_ind, [| typ; x ; typ'; y |]) +let mk_JMeq_refl typ x = mkApp (Lazy.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 = Lazy.force and_typ in + unsafe_fold_right + (fun c conj -> + mkApp (conj_typ, [| c ; conj |])) + l + +let mk_not c = + let notc = Lazy.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 (Lazy.force ex_ind) && Array.length args = 2 -> + let (dom, rng) = + try (args.(0), args.(1)) + with _ -> 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 Rawterm + +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 e -> + Pfedit.delete_current_proof(); + raise e + +(* 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 Termops +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 " : " ++ + print_constr b.rebus ++ fnl ()) + | (mv,Clval(na,b,_)) -> + hov 0 + (pr_meta mv ++ pr_name na ++ str " := " ++ + 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 = print_constr evi.evar_concl in + let pb = + match evi.evar_body with + | Evar_empty -> mt () + | Evar_defined c -> spc() ++ str"=> " ++ 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) -> + print_constr t1 ++ spc() ++ + str (match pbty with + | Reduction.CONV -> "==" + | Reduction.CUMUL -> "<=") ++ + spc() ++ 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(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 new file mode 100644 index 00000000..d0ad334d --- /dev/null +++ b/plugins/subtac/subtac_utils.mli @@ -0,0 +1,136 @@ +open Term +open Libnames +open Coqlib +open Environ +open Pp +open Evd +open Decl_kinds +open Topconstr +open Rawterm +open Util +open Evarutil +open Names +open Sign + +val ($) : ('a -> 'b) -> 'a -> 'b +val contrib_name : string +val subtac_dir : string list +val fix_sub_module : string +val fixsub_module : string list +val init_constant : string list -> string -> constr +val init_reference : string list -> string -> global_reference +val fixsub : constr lazy_t +val well_founded_ref : global_reference lazy_t +val acc_ref : global_reference lazy_t +val acc_inv_ref : global_reference lazy_t +val fix_sub_ref : global_reference lazy_t +val measure_on_R_ref : global_reference lazy_t +val fix_measure_sub_ref : global_reference lazy_t +val refl_ref : global_reference lazy_t +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 lazy_t + +val fix_proto : constr lazy_t +val fix_proto_ref : unit -> constant + +val eq_ind : constr lazy_t +val eq_rec : constr lazy_t +val eq_rect : constr lazy_t +val eq_refl : constr lazy_t + +val not_ref : constr lazy_t +val and_typ : constr lazy_t + +val eqdep_ind : constr lazy_t +val eqdep_rec : constr lazy_t + +val jmeq_ind : constr lazy_t +val jmeq_rec : constr lazy_t +val jmeq_refl : constr lazy_t + +val boolind : constr lazy_t +val sumboolind : constr lazy_t +val natind : constr lazy_t +val intind : constr lazy_t +val existSind : constr lazy_t +val existS : coq_sigma_data lazy_t +val prod : coq_sigma_data lazy_t + +val well_founded : constr lazy_t +val fix : constr lazy_t +val acc : constr lazy_t +val acc_inv : constr lazy_t +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_rawconstr : env -> rawconstr -> 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 lazy_t) 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 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 new file mode 100644 index 00000000..e3dbd127 --- /dev/null +++ b/plugins/subtac/test/ListDep.v @@ -0,0 +1,49 @@ +(* -*- 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 new file mode 100644 index 00000000..2cea0841 --- /dev/null +++ b/plugins/subtac/test/ListsTest.v @@ -0,0 +1,99 @@ +(* -*- 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 new file mode 100644 index 00000000..01e2d75f --- /dev/null +++ b/plugins/subtac/test/Mutind.v @@ -0,0 +1,20 @@ +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 new file mode 100644 index 00000000..7e0755d5 --- /dev/null +++ b/plugins/subtac/test/Test1.v @@ -0,0 +1,16 @@ +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 new file mode 100644 index 00000000..97c3d941 --- /dev/null +++ b/plugins/subtac/test/euclid.v @@ -0,0 +1,24 @@ +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 new file mode 100644 index 00000000..9ae11088 --- /dev/null +++ b/plugins/subtac/test/id.v @@ -0,0 +1,46 @@ +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 new file mode 100644 index 00000000..4f938f4f --- /dev/null +++ b/plugins/subtac/test/measure.v @@ -0,0 +1,20 @@ +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 new file mode 100644 index 00000000..aaefd8cc --- /dev/null +++ b/plugins/subtac/test/rec.v @@ -0,0 +1,65 @@ +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 new file mode 100644 index 00000000..90ae8bae --- /dev/null +++ b/plugins/subtac/test/take.v @@ -0,0 +1,34 @@ +(* -*- 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 new file mode 100644 index 00000000..5ccc154a --- /dev/null +++ b/plugins/subtac/test/wf.v @@ -0,0 +1,48 @@ +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 |