aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/subtac/equations.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac/equations.ml4')
-rw-r--r--plugins/subtac/equations.ml4354
1 files changed, 177 insertions, 177 deletions
diff --git a/plugins/subtac/equations.ml4 b/plugins/subtac/equations.ml4
index 5ae15e00a..ca4445cc2 100644
--- a/plugins/subtac/equations.ml4
+++ b/plugins/subtac/equations.ml4
@@ -8,7 +8,7 @@
(************************************************************************)
(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i camlp4use: "pa_extend.cmo" i*)
+(*i camlp4use: "pa_extend.cmo" i*)
(* $Id$ *)
@@ -40,18 +40,18 @@ type pat =
| 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) ->
+ | PCstr (c, p) ->
let c' = mkConstruct c in
mkApp (c', Array.of_list (constrs_of_pats ~inacc env p))
- | PInac r ->
+ | 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
@@ -59,8 +59,8 @@ let rec pat_vars = function
| PCstr (c, p) -> pats_vars p
| PInac _ -> Intset.empty
-and pats_vars l =
- fold_left (fun vars p ->
+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
@@ -70,7 +70,7 @@ and pats_vars l =
Intset.empty l
let rec pats_of_constrs l = map pat_of_constr l
-and pat_of_constr c =
+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) ->
@@ -95,10 +95,10 @@ let rec pmatch p c =
and pmatches pl l =
match pl, l with
| [], [] -> []
- | hd :: tl, hd' :: tl' ->
+ | 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 =
@@ -108,59 +108,59 @@ let rec pinclude p c =
| PInac _, _ -> true
| _, PInac _ -> true
| _, _ -> false
-
+
and pincludes pl l =
match pl, l with
| [], [] -> true
- | hd :: tl, hd' :: tl' ->
+ | 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 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
+ | 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
+ 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
+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 =
+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 =
+let rec subst_pat env k t p =
match p with
- | PRel i ->
+ | PRel i ->
if i = k then t
else if i > k then PRel (pred i)
else p
@@ -170,9 +170,9 @@ let rec subst_pat env k t p =
and subst_pats env k t = map (subst_pat env k t)
-let rec specialize s p =
+let rec specialize s p =
match p with
- | PRel i ->
+ | PRel i ->
if mem_assoc i s then
let b, t = assoc i s in
if b then PInac t
@@ -190,10 +190,10 @@ let specialize_patterns = function
| s -> specialize_pats s
let specialize_rel_context s ctx =
- snd (fold_right (fun (n, b, t) (k, 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 ->
@@ -202,7 +202,7 @@ let lift_contextn n k sign =
in
liftrec (rel_context_length sign + k) sign
-type program =
+type program =
signature * clause list
and signature = identifier * rel_context * constr
@@ -211,16 +211,16 @@ and clause = lhs * (constr, int) rhs
and lhs = rel_context * identifier * pat list
-and ('a, 'b) rhs =
+and ('a, 'b) rhs =
| Program of 'a
| Empty of 'b
-type splitting =
+type splitting =
| Compute of clause
| Split of lhs * int * inductive_family *
unification_result array * splitting option array
-
-and unification_result =
+
+and unification_result =
rel_context * int * constr * pat * substitution option
and substitution = (int * (bool * constr)) list
@@ -236,14 +236,14 @@ let split_solves split prob =
| Compute (lhs, rhs) -> lhs = prob
| Split (lhs, id, indf, us, ls) -> lhs = prob
-let ids_of_constr c =
- let rec aux vars c =
+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 =
+let ids_of_constrs =
fold_left (fun acc x -> Idset.union (ids_of_constr x) acc) Idset.empty
let idset_of_list =
@@ -252,8 +252,8 @@ let idset_of_list =
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 &&
+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 =
@@ -261,7 +261,7 @@ let check_judgment ctx c t =
let check_context env ctx =
fold_right
- (fun (_, _, t as decl) env ->
+ (fun (_, _, t as decl) env ->
ignore(Typing.sort_of env Evd.empty t); push_rel decl env)
ctx env
@@ -270,7 +270,7 @@ let split_context n c =
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
@@ -284,12 +284,12 @@ let rec add_var_subst env subst n c =
let t = assoc n subst in
if eq_constr t c then subst
else unify env subst t c
- else
+ 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
@@ -298,7 +298,7 @@ and unify env subst x y =
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' =
+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
@@ -306,10 +306,10 @@ and unify_constrs (env : env) subst l l' =
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 ->
+ (fun depth (n,b,t) acc ->
let r = mkRel (depth + k) in
acc || dependent r t ||
(match b with
@@ -319,14 +319,14 @@ let dependent_rel_context (ctx : rel_context) k =
let liftn_between n k p c =
let rec aux depth c = match kind_of_term c with
- | Rel i ->
+ | 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 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)
@@ -348,7 +348,7 @@ let reduce_rel_context (ctx : rel_context) (subst : (int * (bool * constr)) list
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 =
@@ -356,12 +356,12 @@ let rec dependencies_of_rel ctx k =
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 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'))
@@ -374,9 +374,9 @@ let lift_telescope n k 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
@@ -390,7 +390,7 @@ let strengthen (ctx : rel_context) (t : constr) : rel_context * rel_context * (i
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
@@ -412,7 +412,7 @@ let substitute_in_ctx n c ctx =
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
@@ -423,7 +423,7 @@ let rec reduce_subst (ctx : rel_context) (substacc : (int * (bool * constr)) lis
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
+ 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
@@ -439,8 +439,8 @@ let rec reduce_subst (ctx : rel_context) (substacc : (int * (bool * constr)) lis
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) _ ->
@@ -452,7 +452,7 @@ let substituted_context (subst : (int * constr) list) (ctx : rel_context) =
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
@@ -460,11 +460,11 @@ let unify_type before ty =
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 =
+ 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 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
@@ -480,8 +480,8 @@ let unify_type before ty =
env', ctx, constr, constrpat, (* params @ *)args)
cstrs
in
- let res =
- Array.map (fun (env', ctxc, c, cpat, us) ->
+ 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
@@ -490,7 +490,7 @@ let unify_type before ty =
let subst = unify_constrs fullenv [] vs' us in
let subst', ctx' = substituted_context subst fullctx in
(ctx', ctxclen, c, cpat, Some subst')
- with Conflict ->
+ with Conflict ->
(fullctx, ctxclen, c, cpat, None)) cstrs
in Some (res, indf)
with Not_found -> (* not an inductive type *)
@@ -502,35 +502,35 @@ let rec id_of_rel n l =
| n, _ :: tl -> id_of_rel (pred n) tl
| _, _ -> raise (Invalid_argument "id_of_rel")
-let constrs_of_lhs ?(inacc=true) env (ctx, _, pats) =
+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) &&
+
+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
+ | 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) ->
+ | Compute ((ctx, id, lhs), Empty split) ->
let before, (x, _, ty), after = split_context split ctx in
- let unify =
+ let unify =
match unify_type before ty with
- | Some (unify, _) -> unify
+ | Some (unify, _) -> unify
| None -> assert false
in
array_for_all (fun (_, _, _, _, x) -> x = None) unify
-
- | Split ((ctx, id, lhs), rel, indf, unifs, ls) ->
+
+ | 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) ->
+ let ok, splits =
+ Array.fold_left (fun (ok, splits as acc) (ctx', ctxlen, cstr, cstrpat, subst) ->
match subst with
| None -> acc
| Some subst ->
@@ -540,23 +540,23 @@ and valid_splitting_tree (f, delta, t) = function
(* ignore(check_context env' (subst_context subst before)); *)
(* true *)
(* in *)
- let newdelta =
- subst_context subst (subst_rel_context 0 cstr
+ 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)
+ 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') ->
+ 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 =
+
+let valid_tree (f, delta, t) tree =
valid_splitting (f, delta, t, patvars_of_tele delta) tree
let is_constructor c =
@@ -579,12 +579,12 @@ let find_split (_, _, curpats : lhs) (_, _, patcs : lhs) =
and find_split_pats curpats patcs =
assert(List.length curpats = List.length patcs);
- fold_left2 (fun acc ->
+ 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
@@ -595,13 +595,13 @@ let pr_constr_pat env c =
| _ -> pr
let pr_pat env c =
- try
+ 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 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
@@ -618,18 +618,18 @@ let pr_lhs env (delta, f, 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 ++
+ 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 =
@@ -637,36 +637,36 @@ let pr_clauses 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
+ 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 =
+ let splits =
Array.map (fun (ctx', ctxlen, cstr, cstrpat, s) ->
match s with
| None -> None
- | Some s ->
+ | Some s ->
(* ctx' |- s cstr, s cstrpat *)
let newdelta =
- subst_context s (subst_rel_context 0 cstr
+ subst_context s (subst_rel_context 0 cstr
(lift_contextn ctxlen 1 after)) @ ctx' in
- let liftpats =
+ let liftpats =
(* delta |- curpats -> before; ctxc; id; after |- liftpats *)
- lift_pats ctxlen (succ var) curpats
+ 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
+ subst_pats env var liftpat liftpats
in
let lifts = (* before; ctxc |- s : newdelta ->
before; ctxc; after |- lifts : newdelta ; after *)
@@ -674,8 +674,8 @@ let rec split_on env var (delta, f, curpats as lhs) clauses =
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) ->
+ 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))
@@ -684,11 +684,11 @@ let rec split_on env var (delta, f, curpats as lhs) clauses =
clauses := rest;
if matching = [] then (
(* Try finding a splittable variable *)
- let (id, _) =
- fold_right (fun (id, _, ty as decl) (accid, ctx) ->
- match accid with
+ let (id, _) =
+ fold_right (fun (id, _, ty as decl) (accid, ctx) ->
+ match accid with
| Some _ -> (accid, ctx)
- | None ->
+ | None ->
match unify_type ctx ty with
| Some (unify, indf) ->
if array_for_all (fun (_, _, _, _, x) -> x = None) unify then
@@ -696,13 +696,13 @@ let rec split_on env var (delta, f, curpats as lhs) clauses =
else (None, decl :: ctx)
| None -> (None, decl :: ctx))
newdelta (None, [])
- in
+ in
match id with
| None ->
errorlabstrm "deppat"
(str "Non-exhaustive pattern-matching, no clause found for:" ++ fnl () ++
pr_lhs env newlhs)
- | Some id ->
+ | Some id ->
Some (Compute (newlhs, Empty (fst (lookup_rel_id (out_name id) newdelta))))
) else (
let splitting = make_split_aux env newlhs matching in
@@ -713,14 +713,14 @@ let rec split_on env var (delta, f, curpats as lhs) clauses =
(* 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
+ let split =
+ fold_left (fun acc (lhs', rhs) ->
+ match acc with
| None -> find_split lhs lhs'
| _ -> acc) None clauses
- in
+ in
match split with
| Some var -> split_on env var lhs clauses
| None ->
@@ -742,7 +742,7 @@ and make_split_aux env lhs clauses =
let make_split env (f, delta, t) clauses =
make_split_aux env (delta, f, patvars_of_tele delta) clauses
-
+
open Evd
open Evarutil
@@ -755,18 +755,18 @@ let term_of_tree status isevar env (i, delta, ty) ann tree =
(* | 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) ->
+ | 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"),
+ 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
@@ -774,25 +774,25 @@ let term_of_tree status isevar env (i, delta, ty) ann tree =
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) ->
+
+ | 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 ->
+ let branches =
+ array_map2 (fun (ctx', ctxlen, cstr, cstrpat, subst) split ->
match split with
| Some s -> aux s
- | None ->
+ | 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
+ 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) ->
+ 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
@@ -800,18 +800,18 @@ let term_of_tree status isevar env (i, delta, ty) ann tree =
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"),
+ 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"),
+ 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
+ in
let casetyp = it_mkProd_or_LetIn ty' ctx in
mkCast(case, DEFAULTcast, casetyp), casetyp
@@ -829,9 +829,9 @@ let locate_reference qid =
| SynDef kn -> true
let is_global id =
- try
+ try
locate_reference (qualid_of_ident id)
- with Not_found ->
+ with Not_found ->
false
let is_freevar ids env x =
@@ -841,12 +841,12 @@ let is_freevar ids env x =
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 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
+ 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
@@ -858,11 +858,11 @@ let ids_of_patc c ?(bound=Idset.empty) l =
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' =
+ 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)
+ (Name id, None, ty)
in
decl::ctx, push_rel decl env)
vars ([], env)
@@ -871,7 +871,7 @@ let interp_pats i isevar env impls pat sign recu =
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) ->
+ | 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)
@@ -880,18 +880,18 @@ let interp_pats i isevar env impls pat sign recu =
str "Error parsing pattern: unnexpected left-hand side")
in
isevar := nf_evar_defs !isevar;
- (nf_rel_context_evar ( !isevar) varsctx,
+ (nf_rel_context_evar ( !isevar) varsctx,
nf_env_evar ( !isevar) env',
rev_map (nf_evar ( !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 ->
+ | 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')
+ in ((ctx, i, pats_of_constrs (rev patcs)), rhs')
open Entries
@@ -905,10 +905,10 @@ let contrib_tactics_path =
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,
+
+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 =
@@ -918,14 +918,14 @@ let define_by_eqs with_comp i (l,ann) t nt eqs =
let arity = interp_type_evars isevar env' t in
let sign = nf_rel_context_evar ( !isevar) sign in
let arity = nf_evar ( !isevar) arity in
- let arity =
+ 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}
+ const_entry_boxed = false}
in
let c =
Declare.declare_constant compid (DefinitionEntry ce, IsDefinition Definition)
@@ -937,8 +937,8 @@ let define_by_eqs with_comp i (l,ann) t nt eqs =
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 () ->
+ 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
@@ -961,21 +961,21 @@ let define_by_eqs with_comp i (l,ann) t nt eqs =
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
+ 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' =
+ let obls, t', ty' =
Eterm.eterm_obligations env i !isevar ( undef) 0 ~status t ty
in
if is_recursive then
- ignore(Subtac_obligations.add_mutual_definitions [(i, t', ty', impls, obls)] []
+ 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
@@ -993,7 +993,7 @@ struct
end
open Rawterm
-open DeppatGram
+open DeppatGram
open Util
open Pcoq
open Prim
@@ -1002,7 +1002,7 @@ open G_vernac
GEXTEND Gram
GLOBAL: (* deppat_gallina_loc *) deppat_equations binders_let2;
-
+
deppat_equations:
[ [ l = LIST1 equation SEP ";" -> l ] ]
;
@@ -1020,7 +1020,7 @@ GEXTEND Gram
|":="; c = Constr.lconstr -> Program c
] ]
;
-
+
END
type 'a deppat_equations_argtype = (equation list, 'a) Genarg.abstract_argument_type
@@ -1059,8 +1059,8 @@ VERNAC COMMAND EXTEND Define_equations2
decl_notation(nt) ] ->
[ equations false i l t nt eqs ]
END
-
-let rec int_of_coq_nat c =
+
+let rec int_of_coq_nat c =
match kind_of_term c with
| App (f, [| arg |]) -> succ (int_of_coq_nat arg)
| _ -> 0
@@ -1076,24 +1076,24 @@ let solve_equations_goal destruct_tac tac gl =
| _ -> error "Unnexpected goal")
| _ -> error "Unnexpected goal"
in
- let branches, b =
+ 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) ->
+ | 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
+ 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 =
+ 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
@@ -1110,7 +1110,7 @@ let specialize_hyp id gl =
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) ->
+ | 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
@@ -1124,14 +1124,14 @@ let specialize_hyp id gl =
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
+ 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
+ in
+ try
let acc, worked, ty = aux false (mkVar id) ty in
let ty = Evarutil.nf_isevar !evars ty in
if worked then
@@ -1140,9 +1140,9 @@ let specialize_hyp id gl =
(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) ] -> [
+[ "specialize_hypothesis" constr(c) ] -> [
match kind_of_term c with
| Var id -> specialize_hyp id
| _ -> tclFAIL 0 (str "Not an hypothesis") ]
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 10:57:53 +0000