diff options
Diffstat (limited to 'contrib/subtac')
34 files changed, 0 insertions, 7671 deletions
diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4 deleted file mode 100644 index 9d120019..00000000 --- a/contrib/subtac/equations.ml4 +++ /dev/null @@ -1,1149 +0,0 @@ -(* -*- 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 *) -(************************************************************************) - -(*i camlp4deps: "parsing/grammar.cma" i*) -(*i camlp4use: "pa_extend.cmo" i*) - -(* $Id: subtac_cases.ml 11198 2008-07-01 17:03:43Z msozeau $ *) - -open Cases -open Util -open Names -open Nameops -open Term -open Termops -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 List -open Libnames - -type pat = - | PRel of int - | PCstr of constructor * pat list - | PInac of constr - -let coq_inacc = lazy (Coqlib.gen_constant "equations" ["Program";"Equality"] "inaccessible_pattern") - -let mkInac env c = - mkApp (Lazy.force coq_inacc, [| Typing.type_of env Evd.empty c ; c |]) - -let rec constr_of_pat ?(inacc=true) env = function - | PRel i -> mkRel i - | PCstr (c, p) -> - let c' = mkConstruct c in - mkApp (c', Array.of_list (constrs_of_pats ~inacc env p)) - | PInac r -> - if inacc then try mkInac env r with _ -> r else r - -and constrs_of_pats ?(inacc=true) env l = map (constr_of_pat ~inacc env) l - -let rec pat_vars = function - | PRel i -> Intset.singleton i - | PCstr (c, p) -> pats_vars p - | PInac _ -> Intset.empty - -and pats_vars l = - fold_left (fun vars p -> - let pvars = pat_vars p in - let inter = Intset.inter pvars vars in - if inter = Intset.empty then - Intset.union pvars vars - else error ("Non-linear pattern: variable " ^ - string_of_int (Intset.choose inter) ^ " appears twice")) - Intset.empty l - -let rec pats_of_constrs l = map pat_of_constr l -and pat_of_constr c = - match kind_of_term c with - | Rel i -> PRel i - | App (f, [| a ; c |]) when eq_constr f (Lazy.force coq_inacc) -> - PInac c - | App (f, args) when isConstruct f -> - PCstr (destConstruct f, pats_of_constrs (Array.to_list args)) - | Construct f -> PCstr (f, []) - | _ -> PInac c - -let inaccs_of_constrs l = map (fun x -> PInac x) l - -exception Conflict - -let rec pmatch p c = - match p, c with - | PRel i, t -> [i, t] - | PCstr (c, pl), PCstr (c', pl') when c = c' -> pmatches pl pl' - | PInac _, _ -> [] - | _, PInac _ -> [] - | _, _ -> raise Conflict - -and pmatches pl l = - match pl, l with - | [], [] -> [] - | hd :: tl, hd' :: tl' -> - pmatch hd hd' @ pmatches tl tl' - | _ -> raise Conflict - -let pattern_matches pl l = try Some (pmatches pl l) with Conflict -> None - -let rec pinclude p c = - match p, c with - | PRel i, t -> true - | PCstr (c, pl), PCstr (c', pl') when c = c' -> pincludes pl pl' - | PInac _, _ -> true - | _, PInac _ -> true - | _, _ -> false - -and pincludes pl l = - match pl, l with - | [], [] -> true - | hd :: tl, hd' :: tl' -> - pinclude hd hd' && pincludes tl tl' - | _ -> false - -let pattern_includes pl l = pincludes pl l - -(** Specialize by a substitution. *) - -let subst_tele s = replace_vars (List.map (fun (id, _, t) -> id, t) s) - -let subst_rel_subst k s c = - let rec aux depth c = - match kind_of_term c with - | Rel n -> - let k = n - depth in - if k >= 0 then - try lift depth (snd (assoc k s)) - with Not_found -> c - else c - | _ -> map_constr_with_binders succ aux depth c - in aux k c - -let subst_context s ctx = - let (_, ctx') = fold_right - (fun (id, b, t) (k, ctx') -> - (succ k, (id, Option.map (subst_rel_subst k s) b, subst_rel_subst k s t) :: ctx')) - ctx (0, []) - in ctx' - -let subst_rel_context k cstr ctx = - let (_, ctx') = fold_right - (fun (id, b, t) (k, ctx') -> - (succ k, (id, Option.map (substnl [cstr] k) b, substnl [cstr] k t) :: ctx')) - ctx (k, []) - in ctx' - -let rec lift_pat n k p = - match p with - | PRel i -> - if i >= k then PRel (i + n) - else p - | PCstr(c, pl) -> PCstr (c, lift_pats n k pl) - | PInac r -> PInac (liftn n k r) - -and lift_pats n k = map (lift_pat n k) - -let rec subst_pat env k t p = - match p with - | PRel i -> - if i = k then t - else if i > k then PRel (pred i) - else p - | PCstr(c, pl) -> - PCstr (c, subst_pats env k t pl) - | PInac r -> PInac (substnl [constr_of_pat ~inacc:false env t] (pred k) r) - -and subst_pats env k t = map (subst_pat env k t) - -let rec specialize s p = - match p with - | PRel i -> - if mem_assoc i s then - let b, t = assoc i s in - if b then PInac t - else PRel (destRel t) - else p - | PCstr(c, pl) -> - PCstr (c, specialize_pats s pl) - | PInac r -> PInac (specialize_constr s r) - -and specialize_constr s c = subst_rel_subst 0 s c -and specialize_pats s = map (specialize s) - -let specialize_patterns = function - | [] -> fun p -> p - | s -> specialize_pats s - -let specialize_rel_context s ctx = - snd (fold_right (fun (n, b, t) (k, ctx) -> - (succ k, (n, Option.map (subst_rel_subst k s) b, subst_rel_subst k s t) :: ctx)) - ctx (0, [])) - -let lift_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 - -type program = - signature * clause list - -and signature = identifier * rel_context * constr - -and clause = lhs * (constr, int) rhs - -and lhs = rel_context * identifier * pat list - -and ('a, 'b) rhs = - | Program of 'a - | Empty of 'b - -type splitting = - | Compute of clause - | Split of lhs * int * inductive_family * - unification_result array * splitting option array - -and unification_result = - rel_context * int * constr * pat * substitution option - -and substitution = (int * (bool * constr)) list - -type problem = identifier * lhs - -let rels_of_tele tele = rel_list 0 (List.length tele) - -let patvars_of_tele tele = map (fun c -> PRel (destRel c)) (rels_of_tele tele) - -let split_solves split prob = - match split with - | Compute (lhs, rhs) -> lhs = prob - | Split (lhs, id, indf, us, ls) -> lhs = prob - -let ids_of_constr c = - let rec aux vars c = - match kind_of_term c with - | Var id -> Idset.add id vars - | _ -> fold_constr aux vars c - in aux Idset.empty c - -let ids_of_constrs = - fold_left (fun acc x -> Idset.union (ids_of_constr x) acc) Idset.empty - -let idset_of_list = - fold_left (fun s x -> Idset.add x s) Idset.empty - -let intset_of_list = - fold_left (fun s x -> Intset.add x s) Intset.empty - -let solves split (delta, id, pats as prob) = - split_solves split prob && - Intset.equal (pats_vars pats) (intset_of_list (map destRel (rels_of_tele delta))) - -let check_judgment ctx c t = - ignore(Typing.check (push_rel_context ctx (Global.env ())) Evd.empty c t); true - -let check_context env ctx = - fold_right - (fun (_, _, t as decl) env -> - ignore(Typing.sort_of env Evd.empty t); push_rel decl env) - ctx env - -let split_context n c = - let after, before = list_chop n c in - match before with - | hd :: tl -> after, hd, tl - | [] -> raise (Invalid_argument "split_context") - -let split_tele n (ctx : rel_context) = - let rec aux after n l = - match n, l with - | 0, decl :: before -> before, decl, List.rev after - | n, decl :: before -> aux (decl :: after) (pred n) before - | _ -> raise (Invalid_argument "split_tele") - in aux [] n ctx - -let rec add_var_subst env subst n c = - if mem_assoc n subst then - let t = assoc n subst in - if eq_constr t c then subst - else unify env subst t c - else - let rel = mkRel n in - if rel = c then subst - else if dependent rel c then raise Conflict - else (n, c) :: subst - -and unify env subst x y = - match kind_of_term x, kind_of_term y with - | Rel n, _ -> add_var_subst env subst n y - | _, Rel n -> add_var_subst env subst n x - | App (c, l), App (c', l') when eq_constr c c' -> - unify_constrs env subst (Array.to_list l) (Array.to_list l') - | _, _ -> if eq_constr x y then subst else raise Conflict - -and unify_constrs (env : env) subst l l' = - if List.length l = List.length l' then - fold_left2 (unify env) subst l l' - else raise Conflict - -let fold_rel_context_with_binders f ctx init = - snd (List.fold_right (fun decl (depth, acc) -> - (succ depth, f depth decl acc)) ctx (0, init)) - -let dependent_rel_context (ctx : rel_context) k = - fold_rel_context_with_binders - (fun depth (n,b,t) acc -> - let r = mkRel (depth + k) in - acc || dependent r t || - (match b with - | Some b -> dependent r b - | None -> false)) - ctx false - -let liftn_between n k p c = - let rec aux depth c = match kind_of_term c with - | Rel i -> - if i <= depth then c - else if i-depth > p then c - else mkRel (i - n) - | _ -> map_constr_with_binders succ aux depth c - in aux k c - -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 substnl_rel_context n l = - map_rel_context_with_binders (fun k -> substnl l (n+k-1)) - -let reduce_rel_context (ctx : rel_context) (subst : (int * (bool * constr)) list) = - let _, s, ctx' = - fold_left (fun (k, s, ctx') (n, b, t as decl) -> - match b with - | None -> (succ k, mkRel k :: s, ctx' @ [decl]) - | Some t -> (k, lift (pred k) t :: map (substnl [t] (pred k)) s, subst_rel_context 0 t ctx')) - (1, [], []) ctx - in - let s = rev s in - let s' = map (fun (korig, (b, knew)) -> korig, (b, substl s knew)) subst in - s', ctx' - -(* Compute the transitive closure of the dependency relation for a term in a context *) - -let rec dependencies_of_rel ctx k = - let (n,b,t) = nth ctx (pred k) in - let b = Option.map (lift k) b and t = lift k t in - let bdeps = match b with Some b -> dependencies_of_term ctx b | None -> Intset.empty in - Intset.union (Intset.singleton k) (Intset.union bdeps (dependencies_of_term ctx t)) - -and dependencies_of_term ctx t = - let rels = free_rels t in - Intset.fold (fun i -> Intset.union (dependencies_of_rel ctx i)) rels Intset.empty - -let subst_telescope k cstr ctx = - let (_, ctx') = fold_left - (fun (k, ctx') (id, b, t) -> - (succ k, (id, Option.map (substnl [cstr] k) b, substnl [cstr] k t) :: ctx')) - (k, []) ctx - in rev ctx' - -let lift_telescope n k sign = - let rec liftrec k = function - | (na,c,t)::sign -> - (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (succ k) sign) - | [] -> [] - in liftrec k sign - -type ('a,'b) either = Inl of 'a | Inr of 'b - -let strengthen (ctx : rel_context) (t : constr) : rel_context * rel_context * (int * (int, int) either) list = - let rels = dependencies_of_term ctx t in - let len = length ctx in - let nbdeps = Intset.cardinal rels in - let lifting = len - nbdeps in (* Number of variables not linked to t *) - let rec aux k n acc m rest s = function - | decl :: ctx' -> - if Intset.mem k rels then - let rest' = subst_telescope 0 (mkRel (nbdeps + lifting - pred m)) rest in - aux (succ k) (succ n) (decl :: acc) m rest' ((k, Inl n) :: s) ctx' - else aux (succ k) n (subst_telescope 0 mkProp acc) (succ m) (decl :: rest) ((k, Inr m) :: s) ctx' - | [] -> rev acc, rev rest, s - in aux 1 1 [] 1 [] [] ctx - -let merge_subst (ctx', rest, s) = - let lenrest = length rest in - map (function (k, Inl x) -> (k, (false, mkRel (x + lenrest))) | (k, Inr x) -> k, (false, mkRel x)) s - -(* let simplify_subst s = *) -(* fold_left (fun s (k, t) -> *) -(* match kind_of_term t with *) -(* | Rel n when n = k -> s *) -(* | _ -> (k, t) :: s) *) -(* [] s *) - -let compose_subst s' s = - map (fun (k, (b, t)) -> (k, (b, specialize_constr s' t))) s - -let substitute_in_ctx n c ctx = - let rec aux k after = function - | [] -> [] - | (name, b, t as decl) :: before -> - if k = n then rev after @ (name, Some c, t) :: before - else aux (succ k) (decl :: after) before - in aux 1 [] ctx - -let rec reduce_subst (ctx : rel_context) (substacc : (int * (bool * constr)) list) (cursubst : (int * (bool * constr)) list) = - match cursubst with - | [] -> ctx, substacc - | (k, (b, t)) :: rest -> - if t = mkRel k then reduce_subst ctx substacc rest - else if noccur_between 1 k t then - (* The term to substitute refers only to previous variables. *) - let t' = lift (-k) t in - let ctx' = substitute_in_ctx k t' ctx in - reduce_subst ctx' substacc rest - else (* The term refers to variables declared after [k], so we have - to move these dependencies before [k]. *) - let (minctx, ctxrest, subst as str) = strengthen ctx t in - match assoc k subst with - | Inl _ -> error "Occurs check in substituted_context" - | Inr k' -> - let s = merge_subst str in - let ctx' = ctxrest @ minctx in - let rest' = - let substsubst (k', (b, t')) = - match kind_of_term (snd (assoc k' s)) with - | Rel k'' -> (k'', (b, specialize_constr s t')) - | _ -> error "Non-variable substituted for variable by strenghtening" - in map substsubst ((k, (b, t)) :: rest) - in - reduce_subst ctx' (compose_subst s substacc) rest' (* (compose_subst s ((k, (b, t)) :: rest)) *) - - -let substituted_context (subst : (int * constr) list) (ctx : rel_context) = - let _, subst = - fold_left (fun (k, s) _ -> - try let t = assoc k subst in - (succ k, (k, (true, t)) :: s) - with Not_found -> - (succ k, ((k, (false, mkRel k)) :: s))) - (1, []) ctx - in - let ctx', subst' = reduce_subst ctx subst subst in - reduce_rel_context ctx' subst' - -let unify_type before ty = - try - let envb = push_rel_context before (Global.env()) in - let IndType (indf, args) = find_rectype envb Evd.empty ty in - let ind, params = dest_ind_family indf in - let vs = map (Reduction.whd_betadeltaiota envb) args in - let cstrs = Inductiveops.arities_of_constructors envb ind in - let cstrs = - Array.mapi (fun i ty -> - let ty = prod_applist ty params in - let ctx, ty = decompose_prod_assum ty in - let ctx, ids = - let ids = ids_of_rel_context ctx in - fold_right (fun (n, b, t as decl) (acc, ids) -> - match n with Name _ -> (decl :: acc), ids - | Anonymous -> let id = next_name_away Anonymous ids in - ((Name id, b, t) :: acc), (id :: ids)) - ctx ([], ids) - in - let env' = push_rel_context ctx (Global.env ()) in - let IndType (indf, args) = find_rectype env' Evd.empty ty in - let ind, params = dest_ind_family indf in - let constr = applist (mkConstruct (ind, succ i), params @ rels_of_tele ctx) in - let constrpat = PCstr ((ind, succ i), inaccs_of_constrs params @ patvars_of_tele ctx) in - env', ctx, constr, constrpat, (* params @ *)args) - cstrs - in - let res = - Array.map (fun (env', ctxc, c, cpat, us) -> - let _beforelen = length before and ctxclen = length ctxc in - let fullctx = ctxc @ before in - try - let fullenv = push_rel_context fullctx (Global.env ()) in - let vs' = map (lift ctxclen) vs in - let subst = unify_constrs fullenv [] vs' us in - let subst', ctx' = substituted_context subst fullctx in - (ctx', ctxclen, c, cpat, Some subst') - with Conflict -> - (fullctx, ctxclen, c, cpat, None)) cstrs - in Some (res, indf) - with Not_found -> (* not an inductive type *) - None - -let rec id_of_rel n l = - match n, l with - | 0, (Name id, _, _) :: tl -> id - | n, _ :: tl -> id_of_rel (pred n) tl - | _, _ -> raise (Invalid_argument "id_of_rel") - -let constrs_of_lhs ?(inacc=true) env (ctx, _, pats) = - constrs_of_pats ~inacc (push_rel_context ctx env) pats - -let rec valid_splitting (f, delta, t, pats) tree = - split_solves tree (delta, f, pats) && - valid_splitting_tree (f, delta, t) tree - -and valid_splitting_tree (f, delta, t) = function - | Compute (lhs, Program rhs) -> - let subst = constrs_of_lhs ~inacc:false (Global.env ()) lhs in - ignore(check_judgment (pi1 lhs) rhs (substl subst t)); true - - | Compute ((ctx, id, lhs), Empty split) -> - let before, (x, _, ty), after = split_context split ctx in - let unify = - match unify_type before ty with - | Some (unify, _) -> unify - | None -> assert false - in - array_for_all (fun (_, _, _, _, x) -> x = None) unify - - | Split ((ctx, id, lhs), rel, indf, unifs, ls) -> - let before, (id, _, ty), after = split_tele (pred rel) ctx in - let unify, indf' = Option.get (unify_type before ty) in - assert(indf = indf'); - if not (array_exists (fun (_, _, _, _, x) -> x <> None) unify) then false - else - let ok, splits = - Array.fold_left (fun (ok, splits as acc) (ctx', ctxlen, cstr, cstrpat, subst) -> - match subst with - | None -> acc - | Some subst -> -(* let env' = push_rel_context ctx' (Global.env ()) in *) -(* let ctx_correct = *) -(* ignore(check_context env' (subst_context subst ctxc)); *) -(* ignore(check_context env' (subst_context subst before)); *) -(* true *) -(* in *) - let newdelta = - subst_context subst (subst_rel_context 0 cstr - (lift_contextn ctxlen 0 after)) @ before in - let liftpats = lift_pats ctxlen rel lhs in - let newpats = specialize_patterns subst (subst_pats (Global.env ()) rel cstrpat liftpats) in - (ok, (f, newdelta, newpats) :: splits)) - (true, []) unify - in - let subst = List.map2 (fun (id, _, _) x -> out_name id, x) delta - (constrs_of_pats ~inacc:false (Global.env ()) lhs) - in - let t' = replace_vars subst t in - ok && for_all - (fun (f, delta', pats') -> - array_exists (function None -> false | Some tree -> valid_splitting (f, delta', t', pats') tree) ls) splits - -let valid_tree (f, delta, t) tree = - valid_splitting (f, delta, t, patvars_of_tele delta) tree - -let is_constructor c = - match kind_of_term (fst (decompose_app c)) with - | Construct _ -> true - | _ -> false - -let find_split (_, _, curpats : lhs) (_, _, patcs : lhs) = - let rec find_split_pat curpat patc = - match patc with - | PRel _ -> None - | PCstr (f, args) -> - (match curpat with - | PCstr (f', args') when f = f' -> (* Already split at this level, continue *) - find_split_pats args' args - | PRel i -> (* Split on i *) Some i - | PInac c when isRel c -> Some (destRel c) - | _ -> None) - | PInac _ -> None - - and find_split_pats curpats patcs = - assert(List.length curpats = List.length patcs); - fold_left2 (fun acc -> - match acc with - | None -> find_split_pat | _ -> fun _ _ -> acc) - None curpats patcs - in find_split_pats curpats patcs - -open Pp -open Termops - -let pr_constr_pat env c = - let pr = print_constr_env env c in - match kind_of_term c with - | App _ -> str "(" ++ pr ++ str ")" - | _ -> pr - -let pr_pat env c = - try - let patc = constr_of_pat env c in - try pr_constr_pat env patc with _ -> str"pr_constr_pat raised an exception" - with _ -> str"constr_of_pat raised an exception" - -let pr_context env c = - let pr_decl (id,b,_) = - let bstr = match b with Some b -> str ":=" ++ spc () ++ print_constr_env env b | None -> mt() in - let idstr = match id with Name id -> pr_id id | Anonymous -> str"_" in - idstr ++ bstr - in - prlist_with_sep pr_spc pr_decl (List.rev c) -(* Printer.pr_rel_context env c *) - -let pr_lhs env (delta, f, patcs) = - let env = push_rel_context delta env in - let ctx = pr_context env delta in - (if delta = [] then ctx else str "[" ++ ctx ++ str "]" ++ spc ()) - ++ pr_id f ++ spc () ++ prlist_with_sep spc (pr_pat env) patcs - -let pr_rhs env = function - | Empty var -> spc () ++ str ":=!" ++ spc () ++ print_constr_env env (mkRel var) - | Program rhs -> spc () ++ str ":=" ++ spc () ++ print_constr_env env rhs - -let pr_clause env (lhs, rhs) = - pr_lhs env lhs ++ - (let env' = push_rel_context (pi1 lhs) env in - pr_rhs env' rhs) - -(* let pr_splitting env = function *) -(* | Compute cl -> str "Compute " ++ pr_clause env cl *) -(* | Split (lhs, n, indf, results, splits) -> *) - -(* let pr_unification_result (ctx, n, c, pat, subst) = *) - -(* unification_result array * splitting option array *) - -let pr_clauses env = - prlist_with_sep fnl (pr_clause env) - -let lhs_includes (delta, _, patcs : lhs) (delta', _, patcs' : lhs) = - pattern_includes patcs patcs' - -let lhs_matches (delta, _, patcs : lhs) (delta', _, patcs' : lhs) = - pattern_matches patcs patcs' - -let rec split_on env var (delta, f, curpats as lhs) clauses = - let before, (id, _, ty), after = split_tele (pred var) delta in - let unify, indf = - match unify_type before ty with - | Some r -> r - | None -> assert false (* We decided... so it better be inductive *) - in - let clauses = ref clauses in - let splits = - Array.map (fun (ctx', ctxlen, cstr, cstrpat, s) -> - match s with - | None -> None - | Some s -> - (* ctx' |- s cstr, s cstrpat *) - let newdelta = - subst_context s (subst_rel_context 0 cstr - (lift_contextn ctxlen 1 after)) @ ctx' in - let liftpats = - (* delta |- curpats -> before; ctxc; id; after |- liftpats *) - lift_pats ctxlen (succ var) curpats - in - let liftpat = (* before; ctxc |- cstrpat -> before; ctxc; after |- liftpat *) - lift_pat (pred var) 1 cstrpat - in - let substpat = (* before; ctxc; after |- liftpats[id:=liftpat] *) - subst_pats env var liftpat liftpats - in - let lifts = (* before; ctxc |- s : newdelta -> - before; ctxc; after |- lifts : newdelta ; after *) - map (fun (k,(b,x)) -> (pred var + k, (b, lift (pred var) x))) s - in - let newpats = specialize_patterns lifts substpat in - let newlhs = (newdelta, f, newpats) in - let matching, rest = - fold_right (fun (lhs, rhs as clause) (matching, rest) -> - if lhs_includes newlhs lhs then - (clause :: matching, rest) - else (matching, clause :: rest)) - !clauses ([], []) - in - clauses := rest; - if matching = [] then ( - (* Try finding a splittable variable *) - let (id, _) = - fold_right (fun (id, _, ty as decl) (accid, ctx) -> - match accid with - | Some _ -> (accid, ctx) - | None -> - match unify_type ctx ty with - | Some (unify, indf) -> - if array_for_all (fun (_, _, _, _, x) -> x = None) unify then - (Some id, ctx) - else (None, decl :: ctx) - | None -> (None, decl :: ctx)) - newdelta (None, []) - in - match id with - | None -> - errorlabstrm "deppat" - (str "Non-exhaustive pattern-matching, no clause found for:" ++ fnl () ++ - pr_lhs env newlhs) - | Some id -> - Some (Compute (newlhs, Empty (fst (lookup_rel_id (out_name id) newdelta)))) - ) else ( - let splitting = make_split_aux env newlhs matching in - Some splitting)) - unify - in -(* if !clauses <> [] then *) -(* errorlabstrm "deppat" *) -(* (str "Impossible clauses:" ++ fnl () ++ pr_clauses env !clauses); *) - Split (lhs, var, indf, unify, splits) - -and make_split_aux env lhs clauses = - let split = - fold_left (fun acc (lhs', rhs) -> - match acc with - | None -> find_split lhs lhs' - | _ -> acc) None clauses - in - match split with - | Some var -> split_on env var lhs clauses - | None -> - (match clauses with - | [] -> error "No clauses left" - | [(lhs', rhs)] -> - (* No need to split anymore, fix the environments so that they are correctly aligned. *) - (match lhs_matches lhs' lhs with - | Some s -> - let s = map (fun (x, p) -> x, (true, constr_of_pat ~inacc:false env p)) s in - let rhs' = match rhs with - | Program c -> Program (specialize_constr s c) - | Empty i -> Empty (destRel (snd (assoc i s))) - in Compute ((pi1 lhs, pi2 lhs, specialize_patterns s (pi3 lhs')), rhs') - | None -> anomaly "Non-matching clauses at a leaf of the splitting tree") - | _ -> - errorlabstrm "make_split_aux" - (str "Overlapping clauses:" ++ fnl () ++ pr_clauses env clauses)) - -let make_split env (f, delta, t) clauses = - make_split_aux env (delta, f, patvars_of_tele delta) clauses - -open Evd -open Evarutil - -let lift_substitution n s = map (fun (k, x) -> (k + n, x)) s -let map_substitution s t = map (subst_rel_subst 0 s) t - -let term_of_tree status isevar env (i, delta, ty) ann tree = -(* let envrec = match ann with *) -(* | None -> [] *) -(* | Some (loc, i) -> *) -(* let (n, t) = lookup_rel_id i delta in *) -(* let t' = lift n t in *) - - -(* in *) - let rec aux = function - | Compute ((ctx, _, pats as lhs), Program rhs) -> - let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in - let body = it_mkLambda_or_LetIn rhs ctx and typ = it_mkProd_or_LetIn ty' ctx in - mkCast(body, DEFAULTcast, typ), typ - - | Compute ((ctx, _, pats as lhs), Empty split) -> - let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in - let split = (Name (id_of_string "split"), - Some (Class_tactics.coq_nat_of_int (1 + (length ctx - split))), - Lazy.force Class_tactics.coq_nat) - in - let ty' = it_mkProd_or_LetIn ty' ctx in - let let_ty' = mkLambda_or_LetIn split (lift 1 ty') in - let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark (Define true)) let_ty' in - term, ty' - - | Split ((ctx, _, pats as lhs), rel, indf, unif, sp) -> - let before, decl, after = split_tele (pred rel) ctx in - let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in - let branches = - array_map2 (fun (ctx', ctxlen, cstr, cstrpat, subst) split -> - match split with - | Some s -> aux s - | None -> - (* dead code, inversion will find a proof of False by splitting on the rel'th hyp *) - Class_tactics.coq_nat_of_int rel, Lazy.force Class_tactics.coq_nat) - unif sp - in - let branches_ctx = - Array.mapi (fun i (br, brt) -> (id_of_string ("m_" ^ string_of_int i), Some br, brt)) - branches - in - let n, branches_lets = - Array.fold_left (fun (n, lets) (id, b, t) -> - (succ n, (Name id, Option.map (lift n) b, lift n t) :: lets)) - (0, []) branches_ctx - in - let liftctx = lift_contextn (Array.length branches) 0 ctx in - let case = - let ty = it_mkProd_or_LetIn ty' liftctx in - let ty = it_mkLambda_or_LetIn ty branches_lets in - let nbbranches = (Name (id_of_string "branches"), - Some (Class_tactics.coq_nat_of_int (length branches_lets)), - Lazy.force Class_tactics.coq_nat) - in - let nbdiscr = (Name (id_of_string "target"), - Some (Class_tactics.coq_nat_of_int (length before)), - Lazy.force Class_tactics.coq_nat) - in - let ty = it_mkLambda_or_LetIn (lift 2 ty) [nbbranches;nbdiscr] in - let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark status) ty in - term - in - let casetyp = it_mkProd_or_LetIn ty' ctx in - mkCast(case, DEFAULTcast, casetyp), casetyp - - in aux tree - -open Topconstr -open Constrintern -open Decl_kinds - -type equation = constr_expr * (constr_expr, identifier located) rhs - -let locate_reference qid = - match Nametab.extended_locate qid with - | TrueGlobal ref -> true - | SyntacticDef kn -> true - -let is_global id = - try - locate_reference (make_short_qualid id) - with Not_found -> - false - -let is_freevar ids env x = - try - if Idset.mem x ids then false - else - try ignore(Environ.lookup_named x env) ; false - with _ -> not (is_global x) - with _ -> true - -let ids_of_patc c ?(bound=Idset.empty) l = - let found id bdvars l = - if not (is_freevar bdvars (Global.env ()) (snd id)) then l - else if List.exists (fun (_, id') -> id' = snd id) l then l - else id :: l - in - let rec aux bdvars l c = match c with - | CRef (Ident lid) -> found lid bdvars l - | CNotation (_, "{ _ : _ | _ }", ((CRef (Ident (_, id))) :: _, _)) when not (Idset.mem id bdvars) -> - fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c - | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c - in aux bound l c - -let interp_pats i isevar env impls pat sign recu = - let bound = Idset.singleton i in - let vars = ids_of_patc pat ~bound [] in - let varsctx, env' = - fold_right (fun (loc, id) (ctx, env) -> - let decl = - let ty = e_new_evar isevar env ~src:(loc, BinderType (Name id)) (new_Type ()) in - (Name id, None, ty) - in - decl::ctx, push_rel decl env) - vars ([], env) - in - let pats = - let patenv = match recu with None -> env' | Some ty -> push_named (i, None, ty) env' in - let patt, _ = interp_constr_evars_impls ~evdref:isevar patenv ~impls:([],[]) pat in - match kind_of_term patt with - | App (m, args) -> - if not (eq_constr m (mkRel (succ (length varsctx)))) then - user_err_loc (constr_loc pat, "interp_pats", - str "Expecting a pattern for " ++ pr_id i) - else Array.to_list args - | _ -> user_err_loc (constr_loc pat, "interp_pats", - str "Error parsing pattern: unnexpected left-hand side") - in - isevar := nf_evar_defs !isevar; - (nf_rel_context_evar (Evd.evars_of !isevar) varsctx, - nf_env_evar (Evd.evars_of !isevar) env', - rev_map (nf_evar (Evd.evars_of !isevar)) pats) - -let interp_eqn i isevar env impls sign arity recu (pats, rhs) = - let ctx, env', patcs = interp_pats i isevar env impls pats sign recu in - let rhs' = match rhs with - | Program p -> - let ty = nf_isevar !isevar (substl patcs arity) in - Program (interp_casted_constr_evars isevar env' ~impls p ty) - | Empty lid -> Empty (fst (lookup_rel_id (snd lid) ctx)) - in ((ctx, i, pats_of_constrs (rev patcs)), rhs') - -open Entries - -open Tacmach -open Tacexpr -open Tactics -open Tacticals - -let contrib_tactics_path = - make_dirpath (List.map id_of_string ["Equality";"Program";"Coq"]) - -let tactics_tac s = - make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s) - -let equations_tac = lazy - (Tacinterp.eval_tactic - (TacArg(TacCall(dummy_loc, - ArgArg(dummy_loc, tactics_tac "equations"), [])))) - -let define_by_eqs with_comp i (l,ann) t nt eqs = - let env = Global.env () in - let isevar = ref (create_evar_defs Evd.empty) in - let (env', sign), impls = interp_context_evars isevar env l in - let arity = interp_type_evars isevar env' t in - let sign = nf_rel_context_evar (Evd.evars_of !isevar) sign in - let arity = nf_evar (Evd.evars_of !isevar) arity in - let arity = - if with_comp then - let compid = add_suffix i "_comp" in - let ce = - { const_entry_body = it_mkLambda_or_LetIn arity sign; - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = false} - in - let c = - Declare.declare_constant compid (DefinitionEntry ce, IsDefinition Definition) - in mkApp (mkConst c, rel_vect 0 (length sign)) - else arity - in - let env = Global.env () in - let ty = it_mkProd_or_LetIn arity sign in - let data = Command.compute_interning_datas env Constrintern.Recursive [] [i] [ty] [impls] in - let fixdecls = [(Name i, None, ty)] in - let fixenv = push_rel_context fixdecls env in - let equations = - States.with_heavy_rollback (fun () -> - Option.iter (Command.declare_interning_data data) nt; - map (interp_eqn i isevar fixenv data sign arity None) eqs) () - in - let sign = nf_rel_context_evar (Evd.evars_of !isevar) sign in - let arity = nf_evar (Evd.evars_of !isevar) arity in - let prob = (i, sign, arity) in - let fixenv = nf_env_evar (Evd.evars_of !isevar) fixenv in - let fixdecls = nf_rel_context_evar (Evd.evars_of !isevar) fixdecls in - (* let ce = check_evars fixenv Evd.empty !isevar in *) - (* List.iter (function (_, _, Program rhs) -> ce rhs | _ -> ()) equations; *) - let is_recursive, env' = - let occur_eqn ((ctx, _, _), rhs) = - match rhs with - | Program c -> dependent (mkRel (succ (length ctx))) c - | _ -> false - in if exists occur_eqn equations then true, fixenv else false, env - in - let split = make_split env' prob equations in - (* if valid_tree prob split then *) - let status = (* if is_recursive then Expand else *) Define false in - let t, ty = term_of_tree status isevar env' prob ann split in - let undef = undefined_evars !isevar in - let t, ty = if is_recursive then - (it_mkLambda_or_LetIn t fixdecls, it_mkProd_or_LetIn ty fixdecls) - else t, ty - in - let obls, t', ty' = - Eterm.eterm_obligations env i !isevar (Evd.evars_of undef) 0 ~status t ty - in - if is_recursive then - ignore(Subtac_obligations.add_mutual_definitions [(i, t', ty', impls, obls)] [] - ~tactic:(Lazy.force equations_tac) - (Command.IsFixpoint [None, CStructRec])) - else - ignore(Subtac_obligations.add_definition - ~implicits:impls i t' ty' ~tactic:(Lazy.force equations_tac) obls) - -module Gram = Pcoq.Gram -module Vernac = Pcoq.Vernac_ -module Tactic = Pcoq.Tactic - -module DeppatGram = -struct - let gec s = Gram.Entry.create ("Deppat."^s) - - let deppat_equations : equation list Gram.Entry.e = gec "deppat_equations" - - let binders_let2 : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e = gec "binders_let2" - -(* let where_decl : decl_notation Gram.Entry.e = gec "where_decl" *) - -end - -open Rawterm -open DeppatGram -open Util -open Pcoq -open Prim -open Constr -open G_vernac - -GEXTEND Gram - GLOBAL: (* deppat_gallina_loc *) deppat_equations binders_let2; - - deppat_equations: - [ [ l = LIST1 equation SEP ";" -> l ] ] - ; - - binders_let2: - [ [ l = binders_let_fixannot -> l ] ] - ; - - equation: - [ [ c = Constr.lconstr; r=rhs -> (c, r) ] ] - ; - - rhs: - [ [ ":=!"; id = identref -> Empty id - |":="; c = Constr.lconstr -> Program c - ] ] - ; - - END - -type 'a deppat_equations_argtype = (equation list, 'a) Genarg.abstract_argument_type - -let (wit_deppat_equations : Genarg.tlevel deppat_equations_argtype), - (globwit_deppat_equations : Genarg.glevel deppat_equations_argtype), - (rawwit_deppat_equations : Genarg.rlevel deppat_equations_argtype) = - Genarg.create_arg "deppat_equations" - -type 'a binders_let2_argtype = (local_binder list * (identifier located option * recursion_order_expr), 'a) Genarg.abstract_argument_type - -let (wit_binders_let2 : Genarg.tlevel binders_let2_argtype), - (globwit_binders_let2 : Genarg.glevel binders_let2_argtype), - (rawwit_binders_let2 : Genarg.rlevel binders_let2_argtype) = - Genarg.create_arg "binders_let2" - -type 'a decl_notation_argtype = (Vernacexpr.decl_notation, 'a) Genarg.abstract_argument_type - -let (wit_decl_notation : Genarg.tlevel decl_notation_argtype), - (globwit_decl_notation : Genarg.glevel decl_notation_argtype), - (rawwit_decl_notation : Genarg.rlevel decl_notation_argtype) = - Genarg.create_arg "decl_notation" - -let equations wc i l t nt eqs = - try define_by_eqs wc i l t nt eqs - with e -> msg (Cerrors.explain_exn e) - -VERNAC COMMAND EXTEND Define_equations -| [ "Equations" ident(i) binders_let2(l) ":" lconstr(t) ":=" deppat_equations(eqs) - decl_notation(nt) ] -> - [ equations true i l t nt eqs ] - END - -VERNAC COMMAND EXTEND Define_equations2 -| [ "Equations_nocomp" ident(i) binders_let2(l) ":" lconstr(t) ":=" deppat_equations(eqs) - decl_notation(nt) ] -> - [ equations false i l t nt eqs ] -END - -let rec int_of_coq_nat c = - match kind_of_term c with - | App (f, [| arg |]) -> succ (int_of_coq_nat arg) - | _ -> 0 - -let solve_equations_goal destruct_tac tac gl = - let concl = pf_concl gl in - let targetn, branchesn, targ, brs, b = - match kind_of_term concl with - | LetIn (Name target, targ, _, b) -> - (match kind_of_term b with - | LetIn (Name branches, brs, _, b) -> - target, branches, int_of_coq_nat targ, int_of_coq_nat brs, b - | _ -> error "Unnexpected goal") - | _ -> error "Unnexpected goal" - in - let branches, b = - let rec aux n c = - if n = 0 then [], c - else match kind_of_term c with - | LetIn (Name id, br, brt, b) -> - let rest, b = aux (pred n) b in - (id, br, brt) :: rest, b - | _ -> error "Unnexpected goal" - in aux brs b - in - let ids = targetn :: branchesn :: map pi1 branches in - let cleantac = tclTHEN (intros_using ids) (thin ids) in - let dotac = tclDO (succ targ) intro in - let subtacs = - tclTHENS destruct_tac - (map (fun (id, br, brt) -> tclTHEN (letin_tac None (Name id) br (Some brt) onConcl) tac) branches) - in tclTHENLIST [cleantac ; dotac ; subtacs] gl - -TACTIC EXTEND solve_equations - [ "solve_equations" tactic(destruct) tactic(tac) ] -> [ solve_equations_goal (snd destruct) (snd tac) ] - END - -let coq_eq = Lazy.lazy_from_fun Coqlib.build_coq_eq -let coq_eq_refl = lazy ((Coqlib.build_coq_eq_data ()).Coqlib.refl) - -let coq_heq = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq") -let coq_heq_refl = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl") - -let specialize_hyp id gl = - let env = pf_env gl in - let ty = pf_get_hyp_typ gl id in - let evars = ref (create_evar_defs (project gl)) in - let rec aux in_eqs acc ty = - match kind_of_term ty with - | Prod (_, t, b) -> - (match kind_of_term t with - | App (eq, [| eqty; x; y |]) when eq_constr eq (Lazy.force coq_eq) -> - let pt = mkApp (Lazy.force coq_eq, [| eqty; x; x |]) in - let p = mkApp (Lazy.force coq_eq_refl, [| eqty; x |]) in - if e_conv env evars pt t then - aux true (mkApp (acc, [| p |])) (subst1 p b) - else error "Unconvertible members of an homogeneous equality" - | App (heq, [| eqty; x; eqty'; y |]) when eq_constr heq (Lazy.force coq_heq) -> - let pt = mkApp (Lazy.force coq_heq, [| eqty; x; eqty; x |]) in - let p = mkApp (Lazy.force coq_heq_refl, [| eqty; x |]) in - if e_conv env evars pt t then - aux true (mkApp (acc, [| p |])) (subst1 p b) - else error "Unconvertible members of an heterogeneous equality" - | _ -> - if in_eqs then acc, in_eqs, ty - else - let e = e_new_evar evars env t in - aux false (mkApp (acc, [| e |])) (subst1 e b)) - | t -> acc, in_eqs, ty - in - try - let acc, worked, ty = aux false (mkVar id) ty in - let ty = Evarutil.nf_isevar !evars ty in - if worked then - tclTHENFIRST - (fun g -> Tacmach.internal_cut true id ty g) - (exact_no_check (Evarutil.nf_isevar !evars acc)) gl - else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl - with e -> tclFAIL 0 (Cerrors.explain_exn e) gl - -TACTIC EXTEND specialize_hyp -[ "specialize_hypothesis" constr(c) ] -> [ - match kind_of_term c with - | Var id -> specialize_hyp id - | _ -> tclFAIL 0 (str "Not an hypothesis") ] -END diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml deleted file mode 100644 index 00a69bba..00000000 --- a/contrib/subtac/eterm.ml +++ /dev/null @@ -1,221 +0,0 @@ -(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *) -(** - - 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: Tacexpr.raw_tactic_expr 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 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 (mkVar 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. - A little optimization: don't include unnecessary let-ins and their dependencies. -*) -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 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 -> -(* if noccurn 1 rest then lift (-1) rest, s', trans' *) -(* else *) - let c', s'', trans'' = subst_evar_constr evs n 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 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.sort (fun (_, _, deps) (_, _, deps') -> - if Intset.subset deps deps' then (* deps' depends on deps *) -1 - else if Intset.subset deps' deps then 1 - else Intset.compare deps deps') - evl - -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.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 t - in - let ty, _, _ = subst_evar_constr evts 0 ty in - let evars = - List.map (fun (_, 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 Array.of_list (List.rev evars), t', ty - -let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n - -let etermtac (evm, t) = assert(false) (*eterm evm t None *) diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli deleted file mode 100644 index 19e8ffe8..00000000 --- a/contrib/subtac/eterm.mli +++ /dev/null @@ -1,32 +0,0 @@ -(************************************************************************) -(* 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: eterm.mli 11576 2008-11-10 19:13:15Z msozeau $ 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_defs -> evar_map -> int -> - ?status:obligation_definition_status -> constr -> types -> - (identifier * types * loc * obligation_definition_status * Intset.t * - Tacexpr.raw_tactic_expr option) array * constr * types - (* Obl. name, type as product, location of the original evar, associated tactic, - status and dependencies as indexes into the array *) - -val etermtac : open_constr -> tactic diff --git a/contrib/subtac/g_eterm.ml4 b/contrib/subtac/g_eterm.ml4 deleted file mode 100644 index d9dd42cd..00000000 --- a/contrib/subtac/g_eterm.ml4 +++ /dev/null @@ -1,27 +0,0 @@ -(************************************************************************) -(* 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 *) -(************************************************************************) -(**************************************************************************) -(* *) -(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) -(* *) -(* Pierre Crégut (CNET, Lannion, France) *) -(* *) -(**************************************************************************) - -(*i camlp4deps: "parsing/grammar.cma" i*) - -(* $Id: g_eterm.ml4 8654 2006-03-22 15:36:58Z msozeau $ *) - -open Eterm - -TACTIC EXTEND eterm - [ "eterm" ] -> [ - (fun gl -> - let evm = Tacmach.project gl and t = Tacmach.pf_concl gl in - Eterm.etermtac (evm, t) gl) ] -END diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 deleted file mode 100644 index 7194d435..00000000 --- a/contrib/subtac/g_subtac.ml4 +++ /dev/null @@ -1,156 +0,0 @@ -(************************************************************************) -(* 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: g_subtac.ml4 11576 2008-11-10 19:13:15Z msozeau $ *) - - -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_nameopt : identifier option Gram.Entry.e = gec "subtac_nameopt" -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_nameopt; - - subtac_gallina_loc: - [ [ g = Vernac.gallina -> loc, g - | g = Vernac.gallina_ext -> loc, g ] ] - ; - - subtac_nameopt: - [ [ "ofb"; id=Prim.ident -> Some (id) - | -> 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 nameopt_argtype = (identifier option, 'a) Genarg.abstract_argument_type - -let (wit_subtac_nameopt : Genarg.tlevel nameopt_argtype), - (globwit_subtac_nameopt : Genarg.glevel nameopt_argtype), - (rawwit_subtac_nameopt : Genarg.rlevel nameopt_argtype) = - Genarg.create_arg "subtac_nameopt" - -VERNAC COMMAND EXTEND Subtac -[ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ] - END - -VERNAC COMMAND EXTEND Subtac_Obligations -| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, Some t) ] -| [ "Obligation" integer(num) "of" ident(name) ] -> [ Subtac_obligations.subtac_obligation (num, Some name, None) ] -| [ "Obligation" integer(num) ":" lconstr(t) ] -> [ Subtac_obligations.subtac_obligation (num, None, Some t) ] -| [ "Obligation" integer(num) ] -> [ Subtac_obligations.subtac_obligation (num, None, None) ] -| [ "Next" "Obligation" "of" ident(name) ] -> [ Subtac_obligations.next_obligation (Some name) ] -| [ "Next" "Obligation" ] -> [ Subtac_obligations.next_obligation None ] -END - -VERNAC COMMAND EXTEND Subtac_Solve_Obligation -| [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] -> - [ Subtac_obligations.try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligation" integer(num) "using" tactic(t) ] -> - [ Subtac_obligations.try_solve_obligation num None (Some (Tacinterp.interp t)) ] - END - -VERNAC COMMAND EXTEND Subtac_Solve_Obligations -| [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> - [ Subtac_obligations.try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" "using" tactic(t) ] -> - [ Subtac_obligations.try_solve_obligations None (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" ] -> - [ Subtac_obligations.try_solve_obligations None None ] - END - -VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations -| [ "Solve" "All" "Obligations" "using" tactic(t) ] -> - [ Subtac_obligations.solve_all_obligations (Some (Tacinterp.interp t)) ] -| [ "Solve" "All" "Obligations" ] -> - [ Subtac_obligations.solve_all_obligations None ] - END - -VERNAC COMMAND EXTEND Subtac_Admit_Obligations -| [ "Admit" "Obligations" "of" ident(name) ] -> [ Subtac_obligations.admit_obligations (Some name) ] -| [ "Admit" "Obligations" ] -> [ Subtac_obligations.admit_obligations None ] - END - -VERNAC COMMAND EXTEND Subtac_Set_Solver -| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ - Coqlib.check_required_library ["Coq";"Program";"Tactics"]; - Tacinterp.add_tacdef false - [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligation_tactic"), true, t)] ] -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/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml deleted file mode 100644 index c0b64379..00000000 --- a/contrib/subtac/subtac.ml +++ /dev/null @@ -1,241 +0,0 @@ -(************************************************************************) -(* 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: subtac.ml 12194 2009-06-17 16:38:09Z msozeau $ *) - -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 Dyn -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 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 false (id_of_string "Unnamed_thm") - (Pfedit.get_all_proof_names ()) - in - let evm, c, typ, _imps = - Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None - in - let c = solve_tccs_in_type env id isevars evm c typ in - Command.start_proof id kind c hook - -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_assumption 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 [] (Command.generalize_constr_expr c bl) None - in - let c = solve_tccs_in_type env id isevars evm c typ in - List.iter (Command.declare_one_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_assumption 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)], lettop, hook) -> - 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 (glob, sup, is, props, pri) -> - dump_constraint "inst" is; - 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'' -> raise e) - - | e -> raise e diff --git a/contrib/subtac/subtac.mli b/contrib/subtac/subtac.mli deleted file mode 100644 index b51150aa..00000000 --- a/contrib/subtac/subtac.mli +++ /dev/null @@ -1,2 +0,0 @@ -val require_library : string -> unit -val subtac : Util.loc * Vernacexpr.vernac_expr -> unit diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml deleted file mode 100644 index bd06407f..00000000 --- a/contrib/subtac/subtac_cases.ml +++ /dev/null @@ -1,2032 +0,0 @@ -(* -*- 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: subtac_cases.ml 12194 2009-06-17 16:38:09Z msozeau $ *) - -open Cases -open Util -open Names -open Nameops -open Term -open Termops -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 - -let push_rel_defs = - List.fold_right (fun (x,d,t) e -> push_rel (x,Some d,t) e) - -(* 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 initial_history = function Continuation (_,[],Top) -> true | _ -> false - -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_defs 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 - - -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 (Evd.evars_of !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 (Evd.evars_of !isevars) j.uj_type in - let t = - try IsInd (typ,find_rectype env (Evd.evars_of !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 (Evd.evars_of !(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 = Evd.evars_of !(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 - -let lift_tomatch n ((current,typ),info) = - ((lift n current,lift_tomatch_type n typ),info) - -(**********************************************************************) -(* 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 unalias_pat = function - | PatVar (c,name) as p -> - if name = Anonymous then p else PatVar (c,Anonymous) - | PatCstr(a,b,c,name) as p -> - if name = Anonymous then p else PatCstr (a,b,c,Anonymous) - -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 Closure.mind_equiv env 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 liftn_rel_declaration n k = map_rel_declaration (liftn n k) -let substnl_rel_declaration sigma k = map_rel_declaration (substnl sigma k) - -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) (Evd.evars_of 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 - lam_it 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 (Evd.evars_of !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 (evars_of 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 (Evd.evars_of !isevars) indf current tms p - | None -> infer_predicate loc env isevars typs cstrs indf in - let typ = whd_beta (Evd.evars_of !isevars) (applist (pred, realargs)) in - if dep then - (pred, whd_beta (Evd.evars_of !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 (Evd.evars_of !(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 (Evd.evars_of !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 (evars_of 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 (Evd.evars_of !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_from 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_from 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 hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true)) - -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 - -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, _) = find_rectype env (Evd.evars_of !isevars) (lift (-(List.length realargs)) 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 (Evd.evars_of !isevars) app in - let IndType (indf, realargs) = find_rectype env (Evd.evars_of !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_from 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 = - let prev, ctx, names = - List.fold_left - (fun (prev, ctx, names) (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 - | _ -> - let name = next_ident_away_from (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) - ([], [], []) tomatchs - in List.rev prev, ctx - -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 (Environ.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 evar_defs (env : env) : env = - let nf t = nf_isevar evar_defs 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 - -(* 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 _ when not (dependent tm c) - && signlen > 1 (* The term is of a dependent type but does not appear in - the tycon, maybe some variable in its type does. *) -> - (match tmtype with - NotInd _ -> (* len - signlen, subst*) assert false (* signlen > 1 *) - | IsInd (_, IndType(indf,realargs)) -> - 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 - - -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_isevar !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 (Evd.evars_of !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 tomatchs, tomatchs_lets = abstract_tomatch env tomatchs in - let tomatchs_len = List.length tomatchs_lets 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 (Evd.evars_of !isevars) avoid tomatchs arsign - - in - let tycon, arity = - match valcon_of_tycon tycon with - | None -> let ev = mkExistential env isevars in ev, ev - | Some t -> - t, prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars) - tomatchs sign (lift tomatchs_len 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_isevar !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/contrib/subtac/subtac_cases.mli b/contrib/subtac/subtac_cases.mli deleted file mode 100644 index 6b8a0981..00000000 --- a/contrib/subtac/subtac_cases.mli +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* 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: subtac_cases.mli 10739 2008-04-01 14:45:20Z herbelin $ 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/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml deleted file mode 100644 index 9b692d85..00000000 --- a/contrib/subtac/subtac_classes.ml +++ /dev/null @@ -1,194 +0,0 @@ -(************************************************************************) -(* 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: subtac_classes.ml 12187 2009-06-13 19:36:59Z msozeau $ 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_binder_evars evdref env na t = - let t = Constrintern.intern_gen true (Evd.evars_of !evdref) env t in - SPretyping.understand_tcc_evars evdref env IsType t - -let interp_binders_evars isevars env avoid l = - List.fold_left - (fun (env, ids, params) ((loc, i), t) -> - let n = Name i in - let t' = interp_binder_evars isevars env n t in - let d = (i,None,t') in - (push_named d env, i :: ids, d::params)) - (env, avoid, []) l - -let interp_typeclass_context_evars isevars env avoid l = - List.fold_left - (fun (env, ids, params) (iid, bk, cl) -> - let t' = interp_binder_evars isevars env (snd iid) cl in - let i = match snd iid with - | Anonymous -> Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids - | Name id -> id - in - let d = (i,None,t') in - (push_named d env, i :: ids, d::params)) - (env, avoid, []) l - -let interp_constrs_evars isevars env avoid l = - List.fold_left - (fun (env, ids, params) t -> - let t' = interp_binder_evars isevars env Anonymous t in - let id = Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids in - let d = (id,None,t') in - (push_named d env, id :: ids, d::params)) - (env, avoid, []) l - -let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c = - SPretyping.understand_tcc_evars evdref env kind - (intern_gen (kind=IsType) ~impls (Evd.evars_of !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 type_ctx_instance isevars env ctx inst subst = - List.fold_left2 - (fun (subst, instctx) (na, _, t) ce -> - let t' = substl subst t in - let c = interp_casted_constr_evars isevars env ce t' in - isevars := resolve_typeclasses ~onlyargs:true ~fail:true env !isevars; - let d = na, Some c, t' in - c :: subst, d :: instctx) - (subst, []) (List.rev ctx) inst - -let type_class_instance_params isevars env id n ctx inst subst = - List.fold_left2 - (fun (subst, instctx) (na, _, t) ce -> - let t' = replace_vars subst t in - let c = interp_casted_constr_evars isevars env ce t' in - let d = na, Some c, t' in - (na, c) :: subst, d :: instctx) - (subst, []) (List.rev ctx) inst - -let substitution_of_constrs ctx cstrs = - List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx [] - -let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) pri = - let env = Global.env() in - let isevars = ref (Evd.create_evar_defs 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 - in - let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in - let k, ctx', imps, subst = - let c = Command.generalize_constr_expr tclass ctx in - let c', imps = interp_type_evars_impls ~evdref:isevars env c in - let ctx, c = Sign.decompose_prod_assum c' in - let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in - cl, ctx, imps, (List.rev 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 - Termops.next_global_ident_away false i (Termops.ids_of_context env) - in - let env' = push_rel_context ctx' env in - isevars := Evarutil.nf_evar_defs !isevars; - isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars; - let sigma = Evd.evars_of !isevars in - let subst = List.map (Evarutil.nf_evar sigma) subst in - let subst = - 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; - fs - | _ -> - if List.length k.cl_props <> 1 then - errorlabstrm "new_instance" (Pp.str "Expected a definition for the instance body") - else [(dummy_loc, Nameops.out_name (pi1 (List.hd k.cl_props))), props] - in - match k.cl_props with - | [(na,b,ty)] -> - let term = match props with [] -> CHole (Util.dummy_loc, None) | [(_,f)] -> f | _ -> assert false in - let ty' = substl subst ty in - let c = interp_casted_constr_evars isevars env' term ty' in - c :: subst - | _ -> - let props, rest = - List.fold_left - (fun (props, rest) (id,_,_) -> - try - let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in - let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest 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) - ([], props) k.cl_props - in - if rest <> [] then - unbound_method env' k.cl_impl (fst (List.hd rest)) - else - fst (type_ctx_instance isevars env' k.cl_props props subst) - in - 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 inst_constr, ty_constr = instance_constructor k subst in - isevars := Evarutil.nf_evar_defs !isevars; - let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx') - and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx') - in - isevars := undefined_evars !isevars; - Evarutil.check_evars env Evd.empty !isevars termtype; - let hook vis gr = - let cst = match gr with ConstRef kn -> kn | _ -> assert false in - let inst = Typeclasses.new_instance k pri global cst in - Impargs.declare_manual_implicits false gr ~enriching:false imps; - Typeclasses.add_instance inst - in - let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in - let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in - id, Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls - diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli deleted file mode 100644 index 96a51027..00000000 --- a/contrib/subtac/subtac_classes.mli +++ /dev/null @@ -1,42 +0,0 @@ -(************************************************************************) -(* 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: subtac_classes.mli 11709 2008-12-20 11:42:15Z msozeau $ 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_defs ref -> - Environ.env -> - ('a * Term.constr option * Term.constr) list -> - Topconstr.constr_expr list -> - Term.constr list -> - Term.constr list * - ('a * Term.constr option * 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/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml deleted file mode 100644 index 1bbbfbb1..00000000 --- a/contrib/subtac/subtac_coercion.ml +++ /dev/null @@ -1,504 +0,0 @@ -(* -*- 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: subtac_coercion.ml 11576 2008-11-10 19:13:15Z msozeau $ *) - -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 (evars_of !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 (evars_of !isevars) x and y = nf_evar (evars_of !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.decomp_n_prod env (evars_of !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 (Nameops.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 -> failwith "subtac.coerce': Should have detected equivalence earlier" - | _, _ -> - 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 := evar_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 = evars_of !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 = evars_of !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 (evars_of 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 (evars_of isevars) j.uj_type in - (isevars,apply_coercion env (evars_of 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 (evars_of isevars) j.uj_type in - let j1 = apply_coercion env (evars_of isevars) p j t in - (isevars,type_judgment env (j_nf_evar (evars_of isevars) j1)) - with Not_found -> - error_not_a_type_loc loc env (evars_of isevars) j - - let inh_coerce_to_sort loc env isevars j = - let typ = whd_betadeltaiota env (evars_of 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 (evars_of 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 (evars_of 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 (evars_of evd) (t,c1) in - match v with - Some v -> - let j = apply_coercion env (evars_of 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 (evars_of evd) t), - kind_of_term (whd_betadeltaiota env (evars_of 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) = - let evd = nf_evar_defs evd in - match n with - None -> - let (evd', val') = - try - inh_conv_coerce_to_fail loc env evd rigidonly - (Some (nf_isevar evd cj.uj_val)) - (nf_isevar evd cj.uj_type) (nf_isevar evd t) - with NoCoercion -> - let sigma = evars_of 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.decomp_n_prod env (evars_of 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 = evars_of isevars in - error_cannot_coerce env' sigma (t, t')) - else isevars - with _ -> isevars -end diff --git a/contrib/subtac/subtac_coercion.mli b/contrib/subtac/subtac_coercion.mli deleted file mode 100644 index 5678c10e..00000000 --- a/contrib/subtac/subtac_coercion.mli +++ /dev/null @@ -1,4 +0,0 @@ -open Term -val disc_subset : types -> (types * types) option - -module Coercion : Coercion.S diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml deleted file mode 100644 index c8c7ff72..00000000 --- a/contrib/subtac/subtac_command.ml +++ /dev/null @@ -1,466 +0,0 @@ -open Closure -open RedFlags -open Declarations -open Entries -open Dyn -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 = - isevars := Evarutil.nf_evar_defs !isevars; - Evarutil.nf_isevar !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 (Evd.evars_of !isevars) env c in - let c' = SPretyping.pretype_gen 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 (Evd.evars_of !isevars) env c in - let c' = SPretyping.pretype_gen 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 (Evd.evars_of !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 (Evd.evars_of !sigma) env t in - SPretyping.pretype_gen 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 (Evd.evars_of !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)) :: 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) - -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 _ = *) -(* try debug 2 (str "In named context: " ++ prn (named_context env) ++ str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ *) -(* Ppconstr.pr_binders bl ++ str " : " ++ *) -(* Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++ *) -(* Ppconstr.pr_constr_expr body) *) -(* with _ -> () *) - (* in *) - let (env', binders_rel), impls = interp_context_evars isevars env bl in - let after, ((argname, _, argtyp) as arg), before = - let idx = list_index (Name (snd n)) (List.rev_map (fun (na, _, _) -> na) binders_rel) in - split_args idx binders_rel in - let before_length, after_length = List.length before, List.length after in - let argid = match argname with Name n -> n | _ -> assert(false) in - let liftafter = lift_binders 1 after_length after in - let envwf = push_rel_context before env in - let wf_rel, wf_rel_fun, measure_fn = - let rconstr_body, rconstr = - let app = mkAppC (r, [mkIdentC (id_of_name argname)]) in - let env = push_rel_context [arg] envwf in - let capp = interp_constr isevars env app in - capp, mkLambda (argname, argtyp, capp) - in - trace (str"rconstr_body: " ++ pr rconstr_body); - if measure then - let lt_rel = constr_of_global (Lazy.force lt_ref) in - let name s = Name (id_of_string s) in - let wf_rel_fun lift x y = (* lift to before_env *) - trace (str"lifter rconstr_body:" ++ pr (liftn lift 2 rconstr_body)); - mkApp (lt_rel, [| subst1 x (liftn lift 2 rconstr_body); - subst1 y (liftn lift 2 rconstr_body) |]) - in - let wf_rel = - mkLambda (name "x", argtyp, - mkLambda (name "y", lift 1 argtyp, - wf_rel_fun 0 (mkRel 2) (mkRel 1))) - in - wf_rel, wf_rel_fun , Some rconstr - else rconstr, (fun lift x y -> mkApp (rconstr, [|x; y|])), None - in - let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |]) - in - let argid' = id_of_string (string_of_id argid ^ "'") in - let wfarg len = (Name argid', None, - mkSubset (Name argid') (lift len argtyp) - (wf_rel_fun (succ len) (mkRel 1) (mkRel (len + 1)))) - in - let top_bl = after @ (arg :: before) in - let top_env = push_rel_context top_bl env in - let top_arity = interp_type_evars isevars top_env arityc in - let intern_bl = wfarg 1 :: arg :: before in - let _intern_env = push_rel_context intern_bl env in - let proj = (Lazy.force sig_).Coqlib.proj1 in - let projection = - mkApp (proj, [| argtyp ; - (mkLambda (Name argid', argtyp, - (wf_rel_fun 1 (mkRel 1) (mkRel 3)))) ; - mkRel 1 - |]) - in - let intern_arity = it_mkProd_or_LetIn top_arity after in - (* Intern arity is in top_env = arg :: before *) - let intern_arity = liftn 2 2 intern_arity in -(* trace (str "After lifting arity: " ++ *) -(* my_print_constr (push_rel (Name argid', None, lift 2 argtyp) intern_env) *) -(* intern_arity); *) - (* arity is now in something :: wfarg :: arg :: before - where what refered to arg now refers to something *) - let intern_arity = substl [projection] intern_arity in - (* substitute the projection of wfarg for something *) - let intern_before_env = push_rel_context before env in - let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in - let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in - let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in - let fun_env = push_rel_context fun_bl intern_before_env in - let fun_arity = interp_type_evars isevars fun_env arityc in - let intern_body = interp_casted_constr isevars fun_env body fun_arity in - let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in - let _ = - try trace ((* str "Fun bl: " ++ prr fun_bl ++ spc () ++ *) - str "Intern bl" ++ prr intern_bl ++ spc ()) -(* str "Top bl" ++ prr top_bl ++ spc () ++ *) -(* str "Intern arity: " ++ pr intern_arity ++ *) -(* str "Top arity: " ++ pr top_arity ++ spc () ++ *) -(* str "Intern body " ++ pr intern_body_lam) *) - with _ -> () - in - let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in - (* Lift to get to constant arguments *) - let lift_cst = List.length after + 1 in - let fix_def = - match measure_fn with - None -> - mkApp (constr_of_global (Lazy.force fix_sub_ref), - [| argtyp ; - wf_rel ; - make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ; - lift lift_cst prop ; - lift lift_cst intern_body_lam |]) - | Some f -> - mkApp (constr_of_global (Lazy.force fix_measure_sub_ref), - [| lift lift_cst argtyp ; - lift lift_cst f ; - lift lift_cst prop ; - lift lift_cst intern_body_lam |]) - in - let def_appl = applist (fix_def, gen_rels (after_length + 1)) in - let def = it_mkLambda_or_LetIn def_appl binders_rel in - let typ = it_mkProd_or_LetIn top_arity binders_rel in - let fullcoqc = Evarutil.nf_isevar !isevars def in - let fullctyp = Evarutil.nf_isevar !isevars typ in - let evm = evars_of_term (Evd.evars_of !isevars) Evd.empty fullctyp in - let evm = evars_of_term (Evd.evars_of !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 evars_def evars_typ ~implicits:impls evars - -let nf_evar_context isevars ctx = - List.map (fun (n, b, t) -> - (n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx - -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 = interp_casted_constr_evars evdref env ~impls fix.Command.fix_body ccl in - it_mkLambda_or_LetIn body ctx - -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 = evars_of 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 _ -> () - | _ -> - 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 interp_recursive fixkind l boxed = - let env = Global.env() in - let fixl, ntnl = List.split l in - let kind = if fixkind <> Command.IsCoFixpoint then Fixpoint else CoFixpoint in - let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in - - (* Interp arities allowing for unresolved types *) - let evdref = ref (Evd.create_evar_defs 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 -> (id,None,t) :: env) - [] fixnames fixtypes - in - let env_rec = push_named_context rec_sign env in - - (* Get interpretation metadatas *) - let impls = Command.compute_interning_datas env Constrintern.Recursive [] fixnames fixtypes fiximps in - let notations = List.fold_right Option.List.cons ntnl [] in - - (* Interp bodies with rollback because temp use of notations/implicit *) - let fixdefs = - States.with_state_protection (fun () -> - List.iter (Command.declare_interning_data impls) notations; - list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls) - () in - - (* Instantiate evars and check all are resolved *) - let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in - let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in - let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in - let rec_sign = nf_named_context_evar (evars_of 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 = Evd.evars_of 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 - | Command.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 - | Command.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, out_n n, bl, typ, def) r false ntn false) - - | [(n, CMeasureRec r)], [(((_,id),_,bl,typ,def),ntn)] -> - ignore(build_wellfounded (id, out_n n, bl, typ, def) r true 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 (Command.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 Command.IsCoFixpoint fixl b diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli deleted file mode 100644 index 3a6a351b..00000000 --- a/contrib/subtac/subtac_command.mli +++ /dev/null @@ -1,50 +0,0 @@ -open Pretyping -open Evd -open Environ -open Term -open Topconstr -open Names -open Libnames -open Pp -open Vernacexpr -open Constrintern - -val interp_gen : - typing_constraint -> - evar_defs ref -> - env -> - ?impls:full_implicits_env -> - ?allow_patvar:bool -> - ?ltacvars:ltac_sign -> - constr_expr -> constr -val interp_constr : - evar_defs ref -> - env -> constr_expr -> constr -val interp_type_evars : - evar_defs ref -> - env -> - ?impls:full_implicits_env -> - constr_expr -> constr -val interp_casted_constr_evars : - evar_defs ref -> - env -> - ?impls:full_implicits_env -> - constr_expr -> types -> constr -val interp_open_constr : - evar_defs ref -> env -> constr_expr -> constr -val interp_constr_judgment : - evar_defs ref -> - env -> - constr_expr -> unsafe_judgment -val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list - -val interp_binder : Evd.evar_defs ref -> - Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr - - - -val build_recursive : - (fixpoint_expr * decl_notation) list -> bool -> unit - -val build_corecursive : - (cofixpoint_expr * decl_notation) list -> bool -> unit diff --git a/contrib/subtac/subtac_errors.ml b/contrib/subtac/subtac_errors.ml deleted file mode 100644 index 3bbfe22b..00000000 --- a/contrib/subtac/subtac_errors.ml +++ /dev/null @@ -1,24 +0,0 @@ -open Util -open Pp -open Printer - -type term_pp = Pp.std_ppcmds - -type subtyping_error = - | UncoercibleInferType of loc * term_pp * term_pp - | UncoercibleInferTerm of loc * term_pp * term_pp * term_pp * term_pp - | UncoercibleRewrite of term_pp * term_pp - -type typing_error = - | NonFunctionalApp of loc * term_pp * term_pp * term_pp - | NonConvertible of loc * term_pp * term_pp - | NonSigma of loc * term_pp - | IllSorted of loc * term_pp - -exception Subtyping_error of subtyping_error -exception Typing_error of typing_error - -exception Debug_msg of string - -let typing_error e = raise (Typing_error e) -let subtyping_error e = raise (Subtyping_error e) diff --git a/contrib/subtac/subtac_errors.mli b/contrib/subtac/subtac_errors.mli deleted file mode 100644 index 8d75b9c0..00000000 --- a/contrib/subtac/subtac_errors.mli +++ /dev/null @@ -1,15 +0,0 @@ -type term_pp = Pp.std_ppcmds -type subtyping_error = - UncoercibleInferType of Util.loc * term_pp * term_pp - | UncoercibleInferTerm of Util.loc * term_pp * term_pp * term_pp * term_pp - | UncoercibleRewrite of term_pp * term_pp -type typing_error = - NonFunctionalApp of Util.loc * term_pp * term_pp * term_pp - | NonConvertible of Util.loc * term_pp * term_pp - | NonSigma of Util.loc * term_pp - | IllSorted of Util.loc * term_pp -exception Subtyping_error of subtyping_error -exception Typing_error of typing_error -exception Debug_msg of string -val typing_error : typing_error -> 'a -val subtyping_error : subtyping_error -> 'a diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml deleted file mode 100644 index 3dcd43d2..00000000 --- a/contrib/subtac/subtac_obligations.ml +++ /dev/null @@ -1,596 +0,0 @@ -(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *) -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) - -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 - * Tacexpr.raw_tactic_expr 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 : Tacexpr.raw_tactic_expr option; - } - -type obligations = (obligation array * int) - -type notations = (string * 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 : Command.fixpoint_kind option ; - prg_implicits : (Topconstr.explicitation * (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 = (SecondaryTable ("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 false 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_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 (Subtac_utils.tactics_call "obligation_tactic" []) - -let _ = - Summary.declare_summary "program-tcc-table" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } - -let progmap_union = ProgMap.fold ProgMap.add - -let cache (_, (infos, tac)) = - from_prg := infos; - set_default_tactic tac - -let (input,output) = - declare_object - { (default_object "Program state") with - cache_function = cache; - load_function = (fun _ -> cache); - open_function = (fun _ -> cache); - classify_function = (fun _ -> Dispose); - export_function = (fun x -> Some x) } - -open Evd - -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 false 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"); - 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); - 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 (Sign.decompose_prod_n_assum m fixtype) in - list_map_i (fun i _ -> i) 0 ctx - -let reduce_fix = - Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty - -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 false x) in - snd (decompose_lam_n len subs), snd (decompose_prod_n len 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 (Command.declare_interning_data ([],[])) first.prg_notations; - Flags.if_verbose ppnl (Command.recursive_message kind indexes fixnames); - let gr = List.hd kns in - let kn = match gr with ConstRef kn -> kn | _ -> assert false in - first.prg_hook local gr; kn - -let declare_obligation obl body = - match obl.obl_status with - | Expand -> { obl with obl_body = Some body } - | Define opaque -> - let ce = - { const_entry_body = body; - const_entry_type = Some obl.obl_type; - const_entry_opaque = - (if get_proofs_transparency () then false - else opaque) ; - const_entry_boxed = false} - in - let constant = Declare.declare_constant obl.obl_name - (DefinitionEntry ce,IsProof Property) - in - 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' = - Array.mapi - (fun i (n, t, l, o, d, tac) -> - debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d)); - { obl_name = n ; obl_body = None; - obl_location = l; obl_type = red t; obl_status = o; - obl_deps = d; obl_tac = tac }) - obls - 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 update_state s = -(* msgnl (str "Updating obligations info"); *) - Lib.add_anonymous_leaf (input s) - -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; - let res = - if rem > 0 then Remain rem - else ( - match prg'.prg_deps with - [] -> - let kn = declare_definition prg' in - from_prg := ProgMap.remove prg.prg_name !from_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 - from_prg := List.fold_left - (fun acc x -> - ProgMap.remove x.prg_name acc) !from_prg progs; - Defined (ConstRef kn)) - else Dependent); - in - update_state (!from_prg, !default_tactic_expr); - res - -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 = - 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 - Command.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 { obl with obl_body = Some body } - in - let obls = Array.copy obls in - let _ = obls.(num) <- obl in - match update_obls prg obls (pred rem) 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; - 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) = - 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 - | 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 -> Tacinterp.interp t - | None -> !default_tactic - in - let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in - obls.(i) <- declare_obligation 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", 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 ?(msg=true) n = - let prg = get_prog_err n in - 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_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 b 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 b 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 - from_prg := ProgMap.remove prg.prg_name !from_prg; - 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 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 = - 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 - -let default_tactic () = !default_tactic diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli deleted file mode 100644 index 766af2fa..00000000 --- a/contrib/subtac/subtac_obligations.mli +++ /dev/null @@ -1,63 +0,0 @@ -open Names -open Util -open Libnames -open Evd -open Proof_type - -type obligation_info = - (identifier * Term.types * loc * - obligation_definition_status * Intset.t * Tacexpr.raw_tactic_expr 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 : Tacexpr.glob_tactic_expr -> unit -val default_tactic : unit -> Proof_type.tactic - -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.constr -> Term.types -> - ?implicits:(Topconstr.explicitation * (bool * bool)) list -> - ?kind:Decl_kinds.definition_kind -> - ?tactic:Proof_type.tactic -> - ?hook:Tacexpr.declaration_hook -> obligation_info -> progress - -type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list - -val add_mutual_definitions : - (Names.identifier * Term.constr * Term.types * - (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> - ?tactic:Proof_type.tactic -> - ?kind:Decl_kinds.definition_kind -> - ?hook:Tacexpr.declaration_hook -> - notations -> - Command.fixpoint_kind -> unit - -val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit - -val next_obligation : Names.identifier 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/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml deleted file mode 100644 index 3ae7c95d..00000000 --- a/contrib/subtac/subtac_pretyping.ml +++ /dev/null @@ -1,137 +0,0 @@ -(************************************************************************) -(* 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: subtac_pretyping.ml 12187 2009-06-13 19:36:59Z msozeau $ *) - -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 Dyn - -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_defs !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 evm = evars_of 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 (evars_of evd) env -let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type (evars_of 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 = Command.abstract_constr_expr c bl in - let tycon = - match tycon with - None -> empty_tycon - | Some t -> - let t = Command.generalize_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 (evars_of !isevars) in - let ty = nf_isevar !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 def ty ~implicits:imps ~kind ~hook evars diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli deleted file mode 100644 index ba0b7cd2..00000000 --- a/contrib/subtac/subtac_pretyping.mli +++ /dev/null @@ -1,24 +0,0 @@ -open Term -open Environ -open Names -open Sign -open Evd -open Global -open Topconstr -open Implicit_quantifiers -open Impargs - -module Pretyping : Pretyping.S - -val interp : - Environ.env -> - Evd.evar_defs ref -> - Rawterm.rawconstr -> - Evarutil.type_constraint -> Term.constr * Term.constr - -val subtac_process : env -> evar_defs 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_defs ref -> identifier -> local_binder list -> - constr_expr -> constr_expr option -> Subtac_obligations.progress diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml deleted file mode 100644 index 00d37f35..00000000 --- a/contrib/subtac/subtac_pretyping_F.ml +++ /dev/null @@ -1,641 +0,0 @@ -(* -*- 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: subtac_pretyping_F.ml 11576 2008-11-10 19:13:15Z msozeau $ *) - -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 Dyn -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 isevars = - let (evd',x) = f !isevars in - isevars := evd'; - x - - let evd_comb1 f isevars x = - let (evd',y) = f !isevars x in - isevars := evd'; - y - - let evd_comb2 f isevars x y = - let (evd',z) = f !isevars x y in - isevars := evd'; - z - - let evd_comb3 f isevars x y z = - let (evd',t) = f !isevars x y z in - isevars := 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 isevars 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 isevars (vdefj.(i)).uj_type - (lift lt lar.(i))) then - error_ill_typed_rec_body_loc loc env (evars_of !isevars) - i lna vdefj lar - done - - let check_branches_message loc env isevars c (explft,lft) = - for i = 0 to Array.length explft - 1 do - if not (e_cumul env isevars lft.(i) explft.(i)) then - let sigma = evars_of !isevars 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 isevars j = function - | None -> j_nf_isevar !isevars j - | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j t - - let push_rels vars env = List.fold_right push_rel vars env - - (* - let evar_type_case isevars env ct pt lft p c = - let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c - in check_branches_message isevars 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 pretype_id loc env (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 - List.assoc id lvar - 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=lam_it ccl' sign; uj_type=prod_it s' sign} - - (*************************************************************************) - (* Main pretyping function *) - - let pretype_ref isevars 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 isevars lvar lmeta cstr] attempts to type [cstr] *) - (* in environment [env], with existential variables [(evars_of isevars)] and *) - (* the type constraint tycon *) - let rec pretype (tycon : type_constraint) env isevars 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 isevars - (pretype_ref isevars env ref) - tycon - - | RVar (loc, id) -> - inh_conv_coerce_to_tycon loc env isevars - (pretype_id loc env 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 (evars_of !isevars) 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 (evars_of !isevars) c) in - inh_conv_coerce_to_tycon loc env isevars 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 isevars env ~src:(loc,InternalHole) (new_Type ()) in - { uj_val = e_new_evar isevars 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 isevars 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 isevars lvar ty in - let bd' = pretype (mk_tycon ty'.utj_val) env isevars 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) isevars 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 = push_rec_types (names,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 -> - isevars := Coercion.inh_conv_coerces_to loc env !isevars ftys.(i) tycon) - tycon; - nf_isevar !isevars 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 isevars 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 isevars names ftys vdefj; - let ftys = Array.map (nf_evar (evars_of !isevars)) ftys in - let fdefs = Array.map (fun x -> nf_evar (evars_of !isevars) (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 isevars fixj tycon - - | RSort (loc,s) -> - inh_conv_coerce_to_tycon loc env isevars (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 isevars 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) isevars resj in - let resty = whd_betadeltaiota env (evars_of !isevars) resj.uj_type in - match kind_of_term resty with - | Prod (na,c1,c2) -> - Option.iter (fun ty -> isevars := - Coercion.inh_conv_coerces_to loc env !isevars resty ty) tycon; - let evd, (_, _, tycon) = split_tycon loc env !isevars tycon in - isevars := evd; - let hj = pretype (mk_tycon (nf_isevar !isevars c1)) env isevars lvar c in - let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in - let typ' = nf_isevar !isevars typ in - apply_rec env (n+1) - { uj_val = nf_isevar !isevars value; - uj_type = nf_isevar !isevars typ' } - (Option.map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest - - | _ -> - let hj = pretype empty_tycon env isevars lvar c in - error_cant_apply_not_functional_loc - (join_loc floc argloc) env (evars_of !isevars) - resj [hj] - in - let resj = j_nf_evar (evars_of !isevars) (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 = evars_of !isevars 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 isevars 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') - isevars tycon - in - let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon' in - let dom_valcon = valcon_of_tycon dom in - let j = pretype_type dom_valcon env isevars lvar c1 in - let var = (name,None,j.utj_val) in - let j' = pretype rng (push_rel var env) isevars lvar c2 in - let resj = judge_of_abstraction env name j j' in - inh_conv_coerce_to_tycon loc env isevars resj tycon - - | RProd(loc,name,k,c1,c2) -> - let j = pretype_type empty_valcon env isevars 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' isevars 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 isevars resj tycon - - | RLetIn(loc,name,c1,c2) -> - let j = pretype empty_tycon env isevars 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) isevars 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 isevars lvar c in - let (IndType (indf,realargs)) = - try find_rectype env (evars_of !isevars) cj.uj_type - with Not_found -> - let cloc = loc_of_rawconstr c in - error_case_not_inductive_loc cloc env (evars_of !isevars) 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 isevars lvar p in - let ccl = nf_evar (evars_of !isevars) 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 (evars_of !isevars) lp inst in - let fj = pretype (mk_tycon fty) env_f isevars 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 isevars lvar d in - let f = it_mkLambda_or_LetIn fj.uj_val fsign in - let ccl = nf_evar (evars_of !isevars) 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 (evars_of !isevars) - 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 isevars lvar c in - let (IndType (indf,realargs)) = - try find_rectype env (evars_of !isevars) cj.uj_type - with Not_found -> - let cloc = loc_of_rawconstr c in - error_case_not_inductive_loc cloc env (evars_of !isevars) 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 isevars lvar p in - let ccl = nf_evar (evars_of !isevars) 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 isevars {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 isevars env ~src:(loc,InternalHole) (new_Type ()) - in - it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in - let pred = nf_evar (evars_of !isevars) pred in - let p = nf_evar (evars_of !isevars) 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 isevars 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 isevars -> pretype vtyc env isevars lvar),isevars) - tycon env (* loc *) (po,tml,eqns) - - | RCast(loc,c,k) -> - let cj = - match k with - CastCoerce -> - let cj = pretype empty_tycon env isevars lvar c in - evd_comb1 (Coercion.inh_coerce_to_base loc env) isevars cj - | CastConv (k,t) -> - let tj = pretype_type empty_valcon env isevars lvar t in - let cj = pretype (mk_tycon tj.utj_val) env isevars 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 isevars cj tycon - - | RDynamic (loc,d) -> - if (tag d) = "constr" then - let c = constr_out d in - let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in - j - (*inh_conv_coerce_to_tycon loc env isevars j tycon*) - else - user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic")) - - (* [pretype_type valcon env isevars lvar c] coerces [c] into a type *) - and pretype_type valcon env isevars lvar = function - | RHole loc -> - (match valcon with - | Some v -> - let s = - let sigma = evars_of !isevars 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 v when is_Type (existential_type sigma v) -> - evd_comb1 (define_evar_as_sort) isevars v - | _ -> 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 isevars env ~src:loc (mkSort s); - utj_type = s}) - | c -> - let j = pretype empty_tycon env isevars lvar c in - let loc = loc_of_rawconstr c in - let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) isevars j in - match valcon with - | None -> tj - | Some v -> - if e_cumul env isevars v tj.utj_val then tj - else - error_unexpected_type_loc - (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v - - let pretype_gen_aux isevars 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 isevars lvar c).uj_val - | IsType -> - (pretype_type empty_valcon env isevars lvar c).utj_val in - let evd,_ = consider_remaining_unif_problems env !isevars in - isevars:=evd; - nf_evar (evars_of !isevars) c' - - let pretype_gen isevars env lvar kind c = - let c = pretype_gen_aux isevars env lvar kind c in - isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !isevars; - nf_evar (evars_of !isevars) 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 isevars = ref (create_evar_defs sigma) in - let j = pretype empty_tycon env isevars ([],[]) c in - let j = j_nf_evar (evars_of !isevars) j in - let isevars,_ = consider_remaining_unif_problems env !isevars in - check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); - j - - let understand_judgment_tcc isevars env c = - let j = pretype empty_tycon env isevars ([],[]) c in - let sigma = evars_of !isevars in - let j = j_nf_evar sigma j in - 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 fail_evar sigma env lvar kind c = - let isevars = ref (Evd.create_evar_defs sigma) in - let c = pretype_gen isevars env lvar kind c in - let evd = !isevars in - if fail_evar then check_evars env Evd.empty evd c; - evd, c - - (** Entry points of the high-level type synthesis algorithm *) - - let understand_gen kind sigma env c = - snd (ise_pretype_gen true sigma env ([],[]) kind c) - - let understand sigma env ?expected_type:exptyp c = - snd (ise_pretype_gen true sigma env ([],[]) (OfType exptyp) c) - - let understand_type sigma env c = - snd (ise_pretype_gen false sigma env ([],[]) IsType c) - - let understand_ltac sigma env lvar kind c = - ise_pretype_gen false sigma env lvar kind c - - let understand_tcc_evars evdref env kind c = - pretype_gen evdref env ([],[]) kind c - - let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c = - let ev, t = - if resolve_classes then - ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c - else - let isevars = ref (Evd.create_evar_defs sigma) in - let c = pretype_gen_aux isevars env ([],[]) (OfType exptyp) c in - !isevars, c - in - Evd.evars_of ev, t -end - -module Default : S = SubtacPretyping_F(Coercion.Default) diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml deleted file mode 100644 index 2ee2018e..00000000 --- a/contrib/subtac/subtac_utils.ml +++ /dev/null @@ -1,474 +0,0 @@ -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 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 fix_measure_sub_ref = make_ref fixsub_module "Fix_measure_sub" -let lt_ref = make_ref ["Init";"Peano"] "lt" -let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf" -let refl_ref = make_ref ["Init";"Logic"] "refl_equal" - -let make_ref s = Qualid (dummy_loc, qualid_of_string s) -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 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 () = - check_required_library ["Coq";"Logic";"JMeq"]; - init_constant ["Logic";"JMeq"] "JMeq" - -let jmeq_rec () = - check_required_library ["Coq";"Logic";"JMeq"]; - init_constant ["Logic";"JMeq"] "JMeq_rec" - -let jmeq_refl () = - 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_defs - -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" - -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 - | _ -> - 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 [inj_open (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 (jmeq_ind (), [| typ; x ; typ'; y |]) -let mk_JMeq_refl typ x = mkApp (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 - Command.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_coma (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 (); 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_defs evd = - let pp_evm = - let evars = evars_of 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/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli deleted file mode 100644 index 9c014286..00000000 --- a/contrib/subtac/subtac_utils.mli +++ /dev/null @@ -1,133 +0,0 @@ -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 fix_measure_sub_ref : global_reference lazy_t -val lt_ref : global_reference lazy_t -val lt_wf_ref : global_reference lazy_t -val refl_ref : global_reference lazy_t -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 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 : unit -> constr -val jmeq_rec : unit -> constr -val jmeq_refl : unit -> constr - -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_defs -> 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_defs 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_defs 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_defs : evar_defs -> 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/contrib/subtac/test/ListDep.v b/contrib/subtac/test/ListDep.v deleted file mode 100644 index da612c43..00000000 --- a/contrib/subtac/test/ListDep.v +++ /dev/null @@ -1,49 +0,0 @@ -(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) -Require Import List. -Require Import Coq.Program.Program. - -Set Implicit Arguments. - -Definition sub_list (A : Set) (l' l : list A) := (forall v, In v l' -> In v l) /\ length l' <= length l. - -Lemma sub_list_tl : forall A : Set, forall x (l l' : list A), sub_list (x :: l) l' -> sub_list l l'. -Proof. - intros. - inversion H. - split. - intros. - apply H0. - auto with datatypes. - auto with arith. -Qed. - -Section Map_DependentRecursor. - Variable U V : Set. - Variable l : list U. - Variable f : { x : U | In x l } -> V. - - Obligations Tactic := unfold sub_list in * ; - program_simpl ; intuition. - - Program Fixpoint map_rec ( l' : list U | sub_list l' l ) - { measure length l' } : { r : list V | length r = length l' } := - match l' with - | nil => nil - | cons x tl => let tl' := map_rec tl in - f x :: tl' - end. - - Next Obligation. - destruct_call map_rec. - simpl in *. - subst l'. - simpl ; auto with arith. - Qed. - - Program Definition map : list V := map_rec l. - -End Map_DependentRecursor. - -Extraction map. -Extraction map_rec. - diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v deleted file mode 100644 index 05fc0803..00000000 --- a/contrib/subtac/test/ListsTest.v +++ /dev/null @@ -1,99 +0,0 @@ -(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) -Require Import Coq.Program.Program. -Require Import List. - -Set Implicit Arguments. - -Section Accessors. - Variable A : Set. - - Program Definition myhd : forall (l : list A | length l <> 0), A := - fun l => - match l with - | nil => ! - | hd :: tl => hd - end. - - Program Definition mytail (l : list A | length l <> 0) : list A := - match l with - | nil => ! - | hd :: tl => tl - end. -End Accessors. - -Program Definition test_hd : nat := myhd (cons 1 nil). - -(*Eval compute in test_hd*) -(*Program Definition test_tail : list A := mytail nil.*) - -Section app. - Variable A : Set. - - Program Fixpoint app (l : list A) (l' : list A) { struct l } : - { r : list A | length r = length l + length l' } := - match l with - | nil => l' - | hd :: tl => hd :: (tl ++ l') - end - where "x ++ y" := (app x y). - - Next Obligation. - intros. - destruct_call app ; program_simpl. - Defined. - - Program Lemma app_id_l : forall l : list A, l = nil ++ l. - Proof. - simpl ; auto. - Qed. - - Program Lemma app_id_r : forall l : list A, l = l ++ nil. - Proof. - induction l ; simpl in * ; auto. - rewrite <- IHl ; auto. - Qed. - -End app. - -Extraction app. - -Section Nth. - - Variable A : Set. - - Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A := - match n, l with - | 0, hd :: _ => hd - | S n', _ :: tl => nth tl n' - | _, nil => ! - end. - - Next Obligation. - Proof. - simpl in *. auto with arith. - Defined. - - Next Obligation. - Proof. - inversion H. - Qed. - - Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := - match l, n with - | hd :: _, 0 => hd - | _ :: tl, S n' => nth' tl n' - | nil, _ => ! - end. - Next Obligation. - Proof. - simpl in *. auto with arith. - Defined. - - Next Obligation. - Proof. - intros. - inversion H. - Defined. - -End Nth. - diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v deleted file mode 100644 index ac49ca96..00000000 --- a/contrib/subtac/test/Mutind.v +++ /dev/null @@ -1,20 +0,0 @@ -Require Import List. - -Program Fixpoint f a : { x : nat | x > 0 } := - match a with - | 0 => 1 - | S a' => g a a' - end -with g a b : { x : nat | x > 0 } := - match b with - | 0 => 1 - | S b' => f b' - end. - -Check f. -Check g. - - - - - diff --git a/contrib/subtac/test/Test1.v b/contrib/subtac/test/Test1.v deleted file mode 100644 index 14b80854..00000000 --- a/contrib/subtac/test/Test1.v +++ /dev/null @@ -1,16 +0,0 @@ -Program Definition test (a b : nat) : { x : nat | x = a + b } := - ((a + b) : { x : nat | x = a + b }). -Proof. -intros. -reflexivity. -Qed. - -Print test. - -Require Import List. - -Program hd_opt (l : list nat) : { x : nat | x <> 0 } := - match l with - nil => 1 - | a :: l => a - end. diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v deleted file mode 100644 index 501aa798..00000000 --- a/contrib/subtac/test/euclid.v +++ /dev/null @@ -1,24 +0,0 @@ -Require Import Coq.Program.Program. -Require Import Coq.Arith.Compare_dec. -Notation "( x & y )" := (existS _ x y) : core_scope. - -Require Import Omega. - -Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf lt a} : - { q : nat & { r : nat | a = b * q + r /\ r < b } } := - if le_lt_dec b a then let (q', r) := euclid (a - b) b in - (S q' & r) - else (O & a). - -Next Obligation. - assert(b * S q' = b * q' + b) by auto with arith ; omega. -Defined. - -Program Definition test_euclid : (prod nat nat) := let (q, r) := euclid 4 2 in (q, q). - -Eval lazy beta zeta delta iota in test_euclid. - -Program Definition testsig (a : nat) : { x : nat & { y : nat | x < y } } := - (a & S a). - -Check testsig. diff --git a/contrib/subtac/test/id.v b/contrib/subtac/test/id.v deleted file mode 100644 index 9ae11088..00000000 --- a/contrib/subtac/test/id.v +++ /dev/null @@ -1,46 +0,0 @@ -Require Coq.Arith.Arith. - -Require Import Coq.subtac.Utils. -Program Fixpoint id (n : nat) : { x : nat | x = n } := - match n with - | O => O - | S p => S (id p) - end. -intros ; auto. - -pose (subset_simpl (id p)). -simpl in e. -unfold p0. -rewrite e. -auto. -Defined. - -Check id. -Print id. -Extraction id. - -Axiom le_gt_dec : forall n m, { n <= m } + { n > m }. -Require Import Omega. - -Program Fixpoint id_if (n : nat) { wf n lt }: { x : nat | x = n } := - if le_gt_dec n 0 then 0 - else S (id_if (pred n)). -intros. -auto with arith. -intros. -pose (subset_simpl (id_if (pred n))). -simpl in e. -rewrite e. -induction n ; auto with arith. -Defined. - -Print id_if_instance. -Extraction id_if_instance. - -Notation "( x & y )" := (@existS _ _ x y) : core_scope. - -Program Definition testsig ( a : nat ) : { x : nat & { y : nat | x = y }} := - (a & a). -intros. -auto. -Qed. diff --git a/contrib/subtac/test/measure.v b/contrib/subtac/test/measure.v deleted file mode 100644 index 4f938f4f..00000000 --- a/contrib/subtac/test/measure.v +++ /dev/null @@ -1,20 +0,0 @@ -Notation "( x & y )" := (@existS _ _ x y) : core_scope. -Unset Printing All. -Require Import Coq.Arith.Compare_dec. - -Require Import Coq.Program.Program. - -Fixpoint size (a : nat) : nat := - match a with - 0 => 1 - | S n => S (size n) - end. - -Program Fixpoint test_measure (a : nat) {measure size a} : nat := - match a with - | S (S n) => S (test_measure n) - | 0 | S 0 => a - end. - -Check test_measure. -Print test_measure.
\ No newline at end of file diff --git a/contrib/subtac/test/rec.v b/contrib/subtac/test/rec.v deleted file mode 100644 index aaefd8cc..00000000 --- a/contrib/subtac/test/rec.v +++ /dev/null @@ -1,65 +0,0 @@ -Require Import Coq.Arith.Arith. -Require Import Lt. -Require Import Omega. - -Axiom lt_ge_dec : forall x y : nat, { x < y } + { x >= y }. -(*Proof. - intros. - elim (le_lt_dec y x) ; intros ; auto with arith. -Defined. -*) -Require Import Coq.subtac.FixSub. -Require Import Wf_nat. - -Lemma preda_lt_a : forall a, 0 < a -> pred a < a. -auto with arith. -Qed. - -Program Fixpoint id_struct (a : nat) : nat := - match a with - 0 => 0 - | S n => S (id_struct n) - end. - -Check struct_rec. - - if (lt_ge_dec O a) - then S (wfrec (pred a)) - else O. - -Program Fixpoint wfrec (a : nat) { wf a lt } : nat := - if (lt_ge_dec O a) - then S (wfrec (pred a)) - else O. -intros. -apply preda_lt_a ; auto. - -Defined. - -Extraction wfrec. -Extraction Inline proj1_sig. -Extract Inductive bool => "bool" [ "true" "false" ]. -Extract Inductive sumbool => "bool" [ "true" "false" ]. -Extract Inlined Constant lt_ge_dec => "<". - -Extraction wfrec. -Extraction Inline lt_ge_dec le_lt_dec. -Extraction wfrec. - - -Program Fixpoint structrec (a : nat) { wf a lt } : nat := - match a with - S n => S (structrec n) - | 0 => 0 - end. -intros. -unfold n0. -omega. -Defined. - -Print structrec. -Extraction structrec. -Extraction structrec. - -Definition structrec_fun (a : nat) : nat := structrec a (lt_wf a). -Print structrec_fun. diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v deleted file mode 100644 index 2e17959c..00000000 --- a/contrib/subtac/test/take.v +++ /dev/null @@ -1,34 +0,0 @@ -(* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) -Require Import JMeq. -Require Import List. -Require Import Program. - -Set Implicit Arguments. -Obligations Tactic := idtac. - -Print cons. - -Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } := - match n with - | 0 => nil - | S p => - match l with - | cons hd tl => let rest := take tl p in cons hd rest - | nil => ! - end - end. - -Require Import Omega. -Solve All Obligations. -Next Obligation. - destruct_call take ; program_simpl. -Defined. - -Next Obligation. - intros. - inversion H. -Defined. - - - - diff --git a/contrib/subtac/test/wf.v b/contrib/subtac/test/wf.v deleted file mode 100644 index 49fec2b8..00000000 --- a/contrib/subtac/test/wf.v +++ /dev/null @@ -1,48 +0,0 @@ -Notation "( x & y )" := (@existS _ _ x y) : core_scope. -Unset Printing All. -Require Import Coq.Arith.Compare_dec. - -Require Import Coq.subtac.Utils. - -Ltac one_simpl_hyp := - match goal with - | [H : (`exist _ _ _) = _ |- _] => simpl in H - | [H : _ = (`exist _ _ _) |- _] => simpl in H - | [H : (`exist _ _ _) < _ |- _] => simpl in H - | [H : _ < (`exist _ _ _) |- _] => simpl in H - | [H : (`exist _ _ _) <= _ |- _] => simpl in H - | [H : _ <= (`exist _ _ _) |- _] => simpl in H - | [H : (`exist _ _ _) > _ |- _] => simpl in H - | [H : _ > (`exist _ _ _) |- _] => simpl in H - | [H : (`exist _ _ _) >= _ |- _] => simpl in H - | [H : _ >= (`exist _ _ _) |- _] => simpl in H - end. - -Ltac one_simpl_subtac := - destruct_exists ; - repeat one_simpl_hyp ; simpl. - -Ltac simpl_subtac := do 3 one_simpl_subtac ; simpl. - -Require Import Omega. -Require Import Wf_nat. - -Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt} : - { q : nat & { r : nat | a = b * q + r /\ r < b } } := - if le_lt_dec b a then let (q', r) := euclid (a - b) b in - (S q' & r) - else (O & a). -destruct b ; simpl_subtac. -omega. -simpl_subtac. -assert(x0 * S q' = x0 + x0 * q'). -rewrite <- mult_n_Sm. -omega. -rewrite H2 ; omega. -simpl_subtac. -split ; auto with arith. -omega. -apply lt_wf. -Defined. - -Check euclid_evars_proof.
\ No newline at end of file |