diff options
Diffstat (limited to 'tactics/decl_interp.ml')
| -rw-r--r-- | tactics/decl_interp.ml | 229 |
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} - + |