summaryrefslogtreecommitdiff
path: root/tactics/decl_interp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/decl_interp.ml')
-rw-r--r--tactics/decl_interp.ml229
1 files changed, 112 insertions, 117 deletions
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index 62824670..2b583af4 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: decl_interp.ml 12422 2009-10-27 08:42:49Z corbinea $ i*)
+(*i $Id$ i*)
open Util
open Names
@@ -22,18 +22,18 @@ open Pp
(* INTERN *)
-let raw_app (loc,hd,args) = if args =[] then hd else RApp(loc,hd,args)
+let raw_app (loc,hd,args) = if args =[] then hd else RApp(loc,hd,args)
-let intern_justification_items globs =
+let intern_justification_items globs =
Option.map (List.map (intern_constr globs))
-let intern_justification_method globs =
+let intern_justification_method globs =
Option.map (intern_tactic globs)
let intern_statement intern_it globs st =
{st_label=st.st_label;
st_it=intern_it globs st.st_it}
-
+
let intern_no_bind intern_it globs x =
globs,intern_it globs x
@@ -41,22 +41,22 @@ let intern_constr_or_thesis globs = function
Thesis n -> Thesis n
| This c -> This (intern_constr globs c)
-let add_var id globs=
+let add_var id globs=
let l1,l2=globs.ltacvars in
{globs with ltacvars= (id::l1),(id::l2)}
let add_name nam globs=
- match nam with
+ match nam with
Anonymous -> globs
| Name id -> add_var id globs
-let intern_hyp iconstr globs = function
+let intern_hyp iconstr globs = function
Hvar (loc,(id,topt)) -> add_var id globs,
Hvar (loc,(id,Option.map (intern_constr globs) topt))
| Hprop st -> add_name st.st_label globs,
Hprop (intern_statement iconstr globs st)
-let intern_hyps iconstr globs hyps =
+let intern_hyps iconstr globs hyps =
snd (list_fold_map (intern_hyp iconstr) globs hyps)
let intern_cut intern_it globs cut=
@@ -65,32 +65,32 @@ let intern_cut intern_it globs cut=
cut_by=intern_justification_items nglobs cut.cut_by;
cut_using=intern_justification_method nglobs cut.cut_using}
-let intern_casee globs = function
+let intern_casee globs = function
Real c -> Real (intern_constr globs c)
- | Virtual cut -> Virtual
- (intern_cut (intern_no_bind (intern_statement intern_constr)) globs cut)
+ | Virtual cut -> Virtual
+ (intern_cut (intern_no_bind (intern_statement intern_constr)) globs cut)
let intern_hyp_list args globs =
let intern_one globs (loc,(id,opttyp)) =
(add_var id globs),
(loc,(id,Option.map (intern_constr globs) opttyp)) in
- list_fold_map intern_one globs args
+ list_fold_map intern_one globs args
-let intern_suffices_clause globs (hyps,c) =
+let intern_suffices_clause globs (hyps,c) =
let nglobs,nhyps = list_fold_map (intern_hyp intern_constr) globs hyps in
- nglobs,(nhyps,intern_constr_or_thesis nglobs c)
+ nglobs,(nhyps,intern_constr_or_thesis nglobs c)
-let intern_fundecl args body globs=
+let intern_fundecl args body globs=
let nglobs,nargs = intern_hyp_list args globs in
nargs,intern_constr nglobs body
-
+
let rec add_vars_of_simple_pattern globs = function
CPatAlias (loc,p,id) ->
add_vars_of_simple_pattern (add_var id globs) p
-(* Stdpp.raise_with_loc loc
+(* Stdpp.raise_with_loc loc
(UserError ("simple_pattern",str "\"as\" is not allowed here"))*)
| CPatOr (loc, _)->
- Stdpp.raise_with_loc loc
+ Stdpp.raise_with_loc loc
(UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here"))
| CPatDelimiters (_,_,p) ->
add_vars_of_simple_pattern globs p
@@ -99,26 +99,26 @@ let rec add_vars_of_simple_pattern globs = function
| CPatNotation(_,_,(pl,pll)) ->
List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pll))
| CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs
- | _ -> globs
+ | _ -> globs
let rec intern_bare_proof_instr globs = function
Pthus i -> Pthus (intern_bare_proof_instr globs i)
| Pthen i -> Pthen (intern_bare_proof_instr globs i)
| Phence i -> Phence (intern_bare_proof_instr globs i)
- | Pcut c -> Pcut
- (intern_cut
+ | Pcut c -> Pcut
+ (intern_cut
(intern_no_bind (intern_statement intern_constr_or_thesis)) globs c)
- | Psuffices c ->
+ | Psuffices c ->
Psuffices (intern_cut intern_suffices_clause globs c)
- | Prew (s,c) -> Prew
- (s,intern_cut
- (intern_no_bind (intern_statement intern_constr)) globs c)
+ | Prew (s,c) -> Prew
+ (s,intern_cut
+ (intern_no_bind (intern_statement intern_constr)) globs c)
| Psuppose hyps -> Psuppose (intern_hyps intern_constr globs hyps)
- | Pcase (params,pat,hyps) ->
+ | Pcase (params,pat,hyps) ->
let nglobs,nparams = intern_hyp_list params globs in
let nnglobs= add_vars_of_simple_pattern nglobs pat in
let nhyps = intern_hyps intern_constr_or_thesis nnglobs hyps in
- Pcase (nparams,pat,nhyps)
+ Pcase (nparams,pat,nhyps)
| Ptake witl -> Ptake (List.map (intern_constr globs) witl)
| Pconsider (c,hyps) -> Pconsider (intern_constr globs c,
intern_hyps intern_constr globs hyps)
@@ -130,7 +130,7 @@ let rec intern_bare_proof_instr globs = function
| Plet hyps -> Plet (intern_hyps intern_constr globs hyps)
| Pclaim st -> Pclaim (intern_statement intern_constr globs st)
| Pfocus st -> Pfocus (intern_statement intern_constr globs st)
- | Pdefine (id,args,body) ->
+ | Pdefine (id,args,body) ->
let nargs,nbody = intern_fundecl args body globs in
Pdefine (id,nargs,nbody)
| Pcast (id,typ) ->
@@ -145,10 +145,10 @@ let rec intern_proof_instr globs instr=
let interp_justification_items sigma env =
Option.map (List.map (fun c ->understand sigma env (fst c)))
-let interp_constr check_sort sigma env c =
- if check_sort then
- understand_type sigma env (fst c)
- else
+let interp_constr check_sort sigma env c =
+ if check_sort then
+ understand_type sigma env (fst c)
+ else
understand sigma env (fst c)
let special_whd env =
@@ -162,13 +162,13 @@ let decompose_eq env id =
let whd = special_whd env typ in
match kind_of_term whd with
App (f,args)->
- if eq_constr f _eq && (Array.length args)=3
+ if eq_constr f _eq && (Array.length args)=3
then args.(0)
else error "Previous step is not an equality."
| _ -> error "Previous step is not an equality."
let get_eq_typ info env =
- let typ = decompose_eq env (get_last env) in
+ let typ = decompose_eq env (get_last env) in
typ
let interp_constr_in_type typ sigma env c =
@@ -177,33 +177,28 @@ let interp_constr_in_type typ sigma env c =
let interp_statement interp_it sigma env st =
{st_label=st.st_label;
st_it=interp_it sigma env st.st_it}
-
+
let interp_constr_or_thesis check_sort sigma env = function
Thesis n -> Thesis n
| This c -> This (interp_constr check_sort sigma env c)
-let type_tester_var body typ =
- raw_app(dummy_loc,
- RLambda(dummy_loc,Anonymous,Explicit,typ,
- RSort (dummy_loc,RProp Null)),body)
-
-let abstract_one_hyp inject h raw =
- match h with
- Hvar (loc,(id,None)) ->
+let abstract_one_hyp inject h raw =
+ match h with
+ Hvar (loc,(id,None)) ->
RProd (dummy_loc,Name id, Explicit, RHole (loc,Evd.BinderType (Name id)), raw)
- | Hvar (loc,(id,Some typ)) ->
+ | Hvar (loc,(id,Some typ)) ->
RProd (dummy_loc,Name id, Explicit, fst typ, raw)
- | Hprop st ->
+ | Hprop st ->
RProd (dummy_loc,st.st_label, Explicit, inject st.st_it, raw)
-let rawconstr_of_hyps inject hyps head =
+let rawconstr_of_hyps inject hyps head =
List.fold_right (abstract_one_hyp inject) hyps head
let raw_prop = RSort (dummy_loc,RProp Null)
-
-let rec match_hyps blend names constr = function
+
+let rec match_hyps blend names constr = function
[] -> [],substl names constr
- | hyp::q ->
+ | hyp::q ->
let (name,typ,body)=destProd constr in
let st= {st_label=name;st_it=substl names typ} in
let qnames=
@@ -216,7 +211,7 @@ let rec match_hyps blend names constr = function
let rhyps,head = match_hyps blend qnames body q in
qhyp::rhyps,head
-let interp_hyps_gen inject blend sigma env hyps head =
+let interp_hyps_gen inject blend sigma env hyps head =
let constr=understand sigma env (rawconstr_of_hyps inject hyps head) in
match_hyps blend [] constr hyps
@@ -224,42 +219,42 @@ let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma e
let dummy_prefix= id_of_string "__"
-let rec deanonymize ids =
- function
- PatVar (loc,Anonymous) ->
+let rec deanonymize ids =
+ function
+ PatVar (loc,Anonymous) ->
let (found,known) = !ids in
- let new_id=Nameops.next_ident_away dummy_prefix known in
+ let new_id=Namegen.next_ident_away dummy_prefix known in
let _= ids:= (loc,new_id) :: found , new_id :: known in
PatVar (loc,Name new_id)
- | PatVar (loc,Name id) as pat ->
+ | PatVar (loc,Name id) as pat ->
let (found,known) = !ids in
let _= ids:= (loc,id) :: found , known in
pat
- | PatCstr(loc,cstr,lpat,nam) ->
+ | PatCstr(loc,cstr,lpat,nam) ->
PatCstr(loc,cstr,List.map (deanonymize ids) lpat,nam)
let rec raw_of_pat =
- function
- PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable"
- | PatVar (loc,Name id) ->
+ function
+ PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable"
+ | PatVar (loc,Name id) ->
RVar (loc,id)
- | PatCstr(loc,((ind,_) as cstr),lpat,_) ->
+ | PatCstr(loc,((ind,_) as cstr),lpat,_) ->
let mind= fst (Global.lookup_inductive ind) in
let rec add_params n q =
if n<=0 then q else
add_params (pred n) (RHole(dummy_loc,
Evd.TomatchTypeParameter(ind,n))::q) in
- let args = List.map raw_of_pat lpat in
+ let args = List.map raw_of_pat lpat in
raw_app(loc,RRef(dummy_loc,Libnames.ConstructRef cstr),
- add_params mind.Declarations.mind_nparams args)
-
+ add_params mind.Declarations.mind_nparams args)
+
let prod_one_hyp = function
(loc,(id,None)) ->
- (fun raw ->
+ (fun raw ->
RProd (dummy_loc,Name id, Explicit,
RHole (loc,Evd.BinderType (Name id)), raw))
- | (loc,(id,Some typ)) ->
- (fun raw ->
+ | (loc,(id,Some typ)) ->
+ (fun raw ->
RProd (dummy_loc,Name id, Explicit, fst typ, raw))
let prod_one_id (loc,id) raw =
@@ -270,13 +265,13 @@ let let_in_one_alias (id,pat) raw =
RLetIn (dummy_loc,Name id, raw_of_pat pat, raw)
let rec bind_primary_aliases map pat =
- match pat with
+ match pat with
PatVar (_,_) -> map
| PatCstr(loc,_,lpat,nam) ->
let map1 =
- match nam with
+ match nam with
Anonymous -> map
- | Name id -> (id,pat)::map
+ | Name id -> (id,pat)::map
in
List.fold_left bind_primary_aliases map1 lpat
@@ -288,17 +283,17 @@ let bind_aliases patvars subst patt =
let map1 = bind_secondary_aliases map subst in
List.rev map1
-let interp_pattern env pat_expr =
+let interp_pattern env pat_expr =
let patvars,pats = Constrintern.intern_pattern env pat_expr in
- match pats with
+ match pats with
[] -> anomaly "empty pattern list"
| [subst,patt] ->
(patvars,bind_aliases patvars subst patt,patt)
| _ -> anomaly "undetected disjunctive pattern"
-let rec match_args dest names constr = function
+let rec match_args dest names constr = function
[] -> [],names,substl names constr
- | _::q ->
+ | _::q ->
let (name,typ,body)=dest constr in
let st={st_label=name;st_it=substl names typ} in
let qnames=
@@ -308,9 +303,9 @@ let rec match_args dest names constr = function
let args,bnames,body = match_args dest qnames body q in
st::args,bnames,body
-let rec match_aliases names constr = function
+let rec match_aliases names constr = function
[] -> [],names,substl names constr
- | _::q ->
+ | _::q ->
let (name,c,typ,body)=destLetIn constr in
let st={st_label=name;st_it=(substl names c,substl names typ)} in
let qnames=
@@ -329,7 +324,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
| _ -> error "No proof per cases/induction/inversion in progress." in
let mib,oib=Global.lookup_inductive pinfo.per_ind in
let num_params = pinfo.per_nparams in
- let _ =
+ let _ =
let expected = mib.Declarations.mind_nparams - num_params in
if List.length params <> expected then
errorlabstrm "suppose it is"
@@ -338,12 +333,12 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
str "expected.") in
let app_ind =
let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in
- let rparams = List.map detype_ground pinfo.per_params in
- let rparams_rec =
- List.map
- (fun (loc,(id,_)) ->
- RVar (loc,id)) params in
- let dum_args=
+ let rparams = List.map detype_ground pinfo.per_params in
+ let rparams_rec =
+ List.map
+ (fun (loc,(id,_)) ->
+ RVar (loc,id)) params in
+ let dum_args=
list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark (Evd.Define false)))
oib.Declarations.mind_nrealargs in
raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in
@@ -351,22 +346,22 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
let inject = function
Thesis (Plain) -> Rawterm.RSort(dummy_loc,RProp Null)
| Thesis (For rec_occ) ->
- if not (List.mem rec_occ pat_vars) then
- errorlabstrm "suppose it is"
- (str "Variable " ++ Nameops.pr_id rec_occ ++
+ if not (List.mem rec_occ pat_vars) then
+ errorlabstrm "suppose it is"
+ (str "Variable " ++ Nameops.pr_id rec_occ ++
str " does not occur in pattern.");
Rawterm.RSort(dummy_loc,RProp Null)
| This (c,_) -> c in
let term1 = rawconstr_of_hyps inject hyps raw_prop in
let loc_ids,npatt =
let rids=ref ([],pat_vars) in
- let npatt= deanonymize rids patt in
+ let npatt= deanonymize rids patt in
List.rev (fst !rids),npatt in
let term2 =
RLetIn(dummy_loc,Anonymous,
RCast(dummy_loc,raw_of_pat npatt,
CastConv (DEFAULTcast,app_ind)),term1) in
- let term3=List.fold_right let_in_one_alias aliases term2 in
+ let term3=List.fold_right let_in_one_alias aliases term2 in
let term4=List.fold_right prod_one_id loc_ids term3 in
let term5=List.fold_right prod_one_hyp params term4 in
let constr = understand sigma env term5 in
@@ -375,8 +370,8 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in
let (_,pat_pat,pat_typ,rest1) = destLetIn rest2 in
let blend st st' =
- match st'.st_it with
- Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label}
+ match st'.st_it with
+ Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label}
| This _ -> {st_it = This st.st_it;st_label=st.st_label} in
let thyps = fst (match_hyps blend nam2 (Termops.pop rest1) hyps) in
tparams,{pat_vars=tpatvars;
@@ -388,7 +383,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
let interp_cut interp_it sigma env cut=
let nenv,nstat = interp_it sigma env cut.cut_stat in
- {cut with
+ {cut with
cut_stat=nstat;
cut_by=interp_justification_items sigma nenv cut.cut_by}
@@ -398,7 +393,7 @@ let interp_no_bind interp_it sigma env x =
let interp_suffices_clause sigma env (hyps,cot)=
let (locvars,_) as res =
match cot with
- This (c,_) ->
+ This (c,_) ->
let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) sigma env hyps c in
nhyps,This nc
| Thesis Plain as th -> interp_hyps sigma env hyps,th
@@ -409,26 +404,26 @@ let interp_suffices_clause sigma env (hyps,cot)=
match st.st_label with
Name id -> Environ.push_named (id,None,st.st_it) env0
| _ -> env in
- let nenv = List.fold_right push_one locvars env in
- nenv,res
-
-let interp_casee sigma env = function
+ let nenv = List.fold_right push_one locvars env in
+ nenv,res
+
+let interp_casee sigma env = function
Real c -> Real (understand sigma env (fst c))
- | Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) sigma env cut)
+ | Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) sigma env cut)
let abstract_one_arg = function
(loc,(id,None)) ->
- (fun raw ->
- RLambda (dummy_loc,Name id, Explicit,
+ (fun raw ->
+ RLambda (dummy_loc,Name id, Explicit,
RHole (loc,Evd.BinderType (Name id)), raw))
- | (loc,(id,Some typ)) ->
- (fun raw ->
+ | (loc,(id,Some typ)) ->
+ (fun raw ->
RLambda (dummy_loc,Name id, Explicit, fst typ, raw))
-let rawconstr_of_fun args body =
+let rawconstr_of_fun args body =
List.fold_right abstract_one_arg args (fst body)
-let interp_fun sigma env args body =
+let interp_fun sigma env args body =
let constr=understand sigma env (rawconstr_of_fun args body) in
match_args destLambda [] constr args
@@ -436,22 +431,22 @@ let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = fu
Pthus i -> Pthus (interp_bare_proof_instr info sigma env i)
| Pthen i -> Pthen (interp_bare_proof_instr info sigma env i)
| Phence i -> Phence (interp_bare_proof_instr info sigma env i)
- | Pcut c -> Pcut (interp_cut
- (interp_no_bind (interp_statement
- (interp_constr_or_thesis true)))
- sigma env c)
- | Psuffices c ->
+ | Pcut c -> Pcut (interp_cut
+ (interp_no_bind (interp_statement
+ (interp_constr_or_thesis true)))
+ sigma env c)
+ | Psuffices c ->
Psuffices (interp_cut interp_suffices_clause sigma env c)
- | Prew (s,c) -> Prew (s,interp_cut
- (interp_no_bind (interp_statement
+ | Prew (s,c) -> Prew (s,interp_cut
+ (interp_no_bind (interp_statement
(interp_constr_in_type (get_eq_typ info env))))
- sigma env c)
+ sigma env c)
| Psuppose hyps -> Psuppose (interp_hyps sigma env hyps)
- | Pcase (params,pat,hyps) ->
- let tparams,tpat,thyps = interp_cases info sigma env params pat hyps in
+ | Pcase (params,pat,hyps) ->
+ let tparams,tpat,thyps = interp_cases info sigma env params pat hyps in
Pcase (tparams,tpat,thyps)
- | Ptake witl ->
+ | Ptake witl ->
Ptake (List.map (fun c -> understand sigma env (fst c)) witl)
| Pconsider (c,hyps) -> Pconsider (interp_constr false sigma env c,
interp_hyps sigma env hyps)
@@ -463,15 +458,15 @@ let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = fu
| Plet hyps -> Plet (interp_hyps sigma env hyps)
| Pclaim st -> Pclaim (interp_statement (interp_constr true) sigma env st)
| Pfocus st -> Pfocus (interp_statement (interp_constr true) sigma env st)
- | Pdefine (id,args,body) ->
+ | Pdefine (id,args,body) ->
let nargs,_,nbody = interp_fun sigma env args body in
Pdefine (id,nargs,nbody)
- | Pcast (id,typ) ->
+ | Pcast (id,typ) ->
Pcast(id,interp_constr true sigma env typ)
let rec interp_proof_instr info sigma env instr=
{emph = instr.emph;
instr = interp_bare_proof_instr info sigma env instr.instr}
-
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-27 13:29:13 +0000