diff options
Diffstat (limited to 'contrib/subtac/equations.ml4')
| -rw-r--r-- | contrib/subtac/equations.ml4 | 1149 |
1 files changed, 0 insertions, 1149 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 |