diff options
author | 2015-01-25 14:42:51 +0100 | |
---|---|---|
committer | 2015-01-25 14:42:51 +0100 | |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /plugins/decl_mode/decl_interp.ml | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'plugins/decl_mode/decl_interp.ml')
-rw-r--r-- | plugins/decl_mode/decl_interp.ml | 212 |
1 files changed, 107 insertions, 105 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 60988dd1..1c56586c 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -1,27 +1,29 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names -open Topconstr -open Tacinterp -open Tacmach +open Constrexpr +open Tacintern open Decl_expr open Decl_mode -open Pretyping.Default +open Pretyping open Glob_term open Term +open Vars open Pp -open Compat +open Decl_kinds +open Misctypes (* INTERN *) -let glob_app (loc,hd,args) = if args =[] then hd else GApp(loc,hd,args) +let glob_app (loc,hd,args) = if List.is_empty args then hd else GApp(loc,hd,args) let intern_justification_items globs = Option.map (List.map (intern_constr globs)) @@ -41,8 +43,7 @@ let intern_constr_or_thesis globs = function | This c -> This (intern_constr globs c) let add_var id globs= - let l1,l2=globs.ltacvars in - {globs with ltacvars= (id::l1),(id::l2)} + {globs with ltacvars = Id.Set.add id globs.ltacvars} let add_name nam globs= match nam with @@ -56,7 +57,7 @@ let intern_hyp iconstr globs = function Hprop (intern_statement iconstr globs st) let intern_hyps iconstr globs hyps = - snd (list_fold_map (intern_hyp iconstr) globs hyps) + snd (List.fold_map (intern_hyp iconstr) globs hyps) let intern_cut intern_it globs cut= let nglobs,nstat=intern_it globs cut.cut_stat in @@ -73,10 +74,10 @@ 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 nglobs,nhyps = list_fold_map (intern_hyp intern_constr) globs hyps in + let nglobs,nhyps = List.fold_map (intern_hyp intern_constr) globs hyps in nglobs,(nhyps,intern_constr_or_thesis nglobs c) let intern_fundecl args body globs= @@ -93,10 +94,11 @@ let rec add_vars_of_simple_pattern globs = function (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here")) | CPatDelimiters (_,_,p) -> add_vars_of_simple_pattern globs p - | CPatCstr (_,_,pl) | CPatCstrExpl (_,_,pl) -> - List.fold_left add_vars_of_simple_pattern globs pl - | CPatNotation(_,_,(pl,pll)) -> - List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pll)) + | CPatCstr (_,_,pl1,pl2) -> + List.fold_left add_vars_of_simple_pattern + (List.fold_left add_vars_of_simple_pattern globs pl1) pl2 + | CPatNotation(_,_,(pl,pll),pl') -> + List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pl'::pll)) | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs | _ -> globs @@ -135,33 +137,33 @@ let rec intern_bare_proof_instr globs = function | Pcast (id,typ) -> Pcast (id,intern_constr globs typ) -let rec intern_proof_instr globs instr= +let intern_proof_instr globs instr= {emph = instr.emph; instr = intern_bare_proof_instr globs instr.instr} (* INTERP *) -let interp_justification_items sigma env = - Option.map (List.map (fun c ->understand sigma env (fst c))) +let interp_justification_items env sigma = + Option.map (List.map (fun c -> fst (*FIXME*)(understand env sigma (fst c)))) -let interp_constr check_sort sigma env c = +let interp_constr check_sort env sigma c = if check_sort then - understand_type sigma env (fst c) + fst (understand env sigma ~expected_type:IsType (fst c) (* FIXME *)) else - understand sigma env (fst c) + fst (understand env sigma (fst c)) let special_whd env = let infos=Closure.create_clos_infos Closure.betadeltaiota env in (fun t -> Closure.whd_val infos (Closure.inject t)) -let _eq = Libnames.constr_of_global (Coqlib.glob_eq) +let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq)) let decompose_eq env id = let typ = Environ.named_type id env in 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 (Lazy.force _eq) && Int.equal (Array.length args) 3 then args.(0) else error "Previous step is not an equality." | _ -> error "Previous step is not an equality." @@ -170,30 +172,30 @@ let get_eq_typ info env = let typ = decompose_eq env (get_last env) in typ -let interp_constr_in_type typ sigma env c = - understand sigma env (fst c) ~expected_type:typ +let interp_constr_in_type typ env sigma c = + fst (understand env sigma (fst c) ~expected_type:(OfType typ))(*FIXME*) -let interp_statement interp_it sigma env st = +let interp_statement interp_it env sigma st = {st_label=st.st_label; - st_it=interp_it sigma env st.st_it} + st_it=interp_it env sigma st.st_it} -let interp_constr_or_thesis check_sort sigma env = function +let interp_constr_or_thesis check_sort env sigma = function Thesis n -> Thesis n - | This c -> This (interp_constr check_sort sigma env c) + | This c -> This (interp_constr check_sort env sigma c) let abstract_one_hyp inject h glob = match h with Hvar (loc,(id,None)) -> - GProd (dummy_loc,Name id, Explicit, GHole (loc,Evd.BinderType (Name id)), glob) + GProd (Loc.ghost,Name id, Explicit, GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob) | Hvar (loc,(id,Some typ)) -> - GProd (dummy_loc,Name id, Explicit, fst typ, glob) + GProd (Loc.ghost,Name id, Explicit, fst typ, glob) | Hprop st -> - GProd (dummy_loc,st.st_label, Explicit, inject st.st_it, glob) + GProd (Loc.ghost,st.st_label, Explicit, inject st.st_it, glob) let glob_constr_of_hyps inject hyps head = List.fold_right (abstract_one_hyp inject) hyps head -let glob_prop = GSort (dummy_loc,GProp Null) +let glob_prop = GSort (Loc.ghost,GProp) let rec match_hyps blend names constr = function [] -> [],substl names constr @@ -210,13 +212,13 @@ 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 constr=understand sigma env (glob_constr_of_hyps inject hyps head) in +let interp_hyps_gen inject blend env sigma hyps head = + let constr= fst(*FIXME*) (understand env sigma (glob_constr_of_hyps inject hyps head)) in match_hyps blend [] constr hyps -let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps glob_prop) +let interp_hyps env sigma hyps = fst (interp_hyps_gen fst (fun x _ -> x) env sigma hyps glob_prop) -let dummy_prefix= id_of_string "__" +let dummy_prefix= Id.of_string "__" let rec deanonymize ids = function @@ -234,34 +236,34 @@ let rec deanonymize ids = let rec glob_of_pat = function - PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable" + PatVar (loc,Anonymous) -> anomaly (Pp.str "Anonymous pattern variable") | PatVar (loc,Name id) -> GVar (loc,id) | 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) (GHole(dummy_loc, - Evd.TomatchTypeParameter(ind,n))::q) in + add_params (pred n) (GHole(Loc.ghost, + Evar_kinds.TomatchTypeParameter(ind,n), Misctypes.IntroAnonymous, None)::q) in let args = List.map glob_of_pat lpat in - glob_app(loc,GRef(dummy_loc,Libnames.ConstructRef cstr), + glob_app(loc,GRef(Loc.ghost,Globnames.ConstructRef cstr,None), add_params mind.Declarations.mind_nparams args) let prod_one_hyp = function (loc,(id,None)) -> (fun glob -> - GProd (dummy_loc,Name id, Explicit, - GHole (loc,Evd.BinderType (Name id)), glob)) + GProd (Loc.ghost,Name id, Explicit, + GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob)) | (loc,(id,Some typ)) -> (fun glob -> - GProd (dummy_loc,Name id, Explicit, fst typ, glob)) + GProd (Loc.ghost,Name id, Explicit, fst typ, glob)) let prod_one_id (loc,id) glob = - GProd (dummy_loc,Name id, Explicit, - GHole (loc,Evd.BinderType (Name id)), glob) + GProd (Loc.ghost,Name id, Explicit, + GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob) let let_in_one_alias (id,pat) glob = - GLetIn (dummy_loc,Name id, glob_of_pat pat, glob) + GLetIn (Loc.ghost,Name id, glob_of_pat pat, glob) let rec bind_primary_aliases map pat = match pat with @@ -275,7 +277,7 @@ let rec bind_primary_aliases map pat = List.fold_left bind_primary_aliases map1 lpat let bind_secondary_aliases map subst = - List.fold_left (fun map (ids,idp) -> (ids,List.assoc idp map)::map) map subst + Id.Map.fold (fun ids idp map -> (ids,Id.List.assoc idp map)::map) subst map let bind_aliases patvars subst patt = let map = bind_primary_aliases [] patt in @@ -285,10 +287,10 @@ let bind_aliases patvars subst patt = let interp_pattern env pat_expr = let patvars,pats = Constrintern.intern_pattern env pat_expr in match pats with - [] -> anomaly "empty pattern list" + [] -> anomaly (Pp.str "empty pattern list") | [subst,patt] -> (patvars,bind_aliases patvars subst patt,patt) - | _ -> anomaly "undetected disjunctive pattern" + | _ -> anomaly (Pp.str "undetected disjunctive pattern") let rec match_args dest names constr = function [] -> [],names,substl names constr @@ -314,9 +316,9 @@ let rec match_aliases names constr = function let args,bnames,body = match_aliases qnames body q in st::args,bnames,body -let detype_ground c = Detyping.detype false [] [] c +let detype_ground env c = Detyping.detype false [] env Evd.empty c -let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = +let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = let et,pinfo = match info.pm_stack with Per(et,pi,_,_)::_ -> et,pi @@ -325,31 +327,31 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let num_params = pinfo.per_nparams in let _ = let expected = mib.Declarations.mind_nparams - num_params in - if List.length params <> expected then + if not (Int.equal (List.length params) expected) then errorlabstrm "suppose it is" (str "Wrong number of extra arguments: " ++ - (if expected = 0 then str "none" else int expected) ++ spc () ++ + (if Int.equal expected 0 then str "none" else int expected) ++ spc () ++ str "expected.") in let app_ind = - let rind = GRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in - let rparams = List.map detype_ground pinfo.per_params in + let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind,None) in + let rparams = List.map (detype_ground env) pinfo.per_params in let rparams_rec = List.map (fun (loc,(id,_)) -> GVar (loc,id)) params in let dum_args= - list_tabulate (fun _ -> GHole (dummy_loc,Evd.QuestionMark (Evd.Define false))) - oib.Declarations.mind_nrealargs in - glob_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in + List.init oib.Declarations.mind_nrealargs + (fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false),Misctypes.IntroAnonymous, None)) in + glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in let pat_vars,aliases,patt = interp_pattern env pat in let inject = function - Thesis (Plain) -> Glob_term.GSort(dummy_loc,GProp Null) + Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp) | Thesis (For rec_occ) -> - if not (List.mem rec_occ pat_vars) then + if not (Id.List.mem rec_occ pat_vars) then errorlabstrm "suppose it is" (str "Variable " ++ Nameops.pr_id rec_occ ++ str " does not occur in pattern."); - Glob_term.GSort(dummy_loc,GProp Null) + Glob_term.GSort(Loc.ghost,GProp) | This (c,_) -> c in let term1 = glob_constr_of_hyps inject hyps glob_prop in let loc_ids,npatt = @@ -357,13 +359,13 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let npatt= deanonymize rids patt in List.rev (fst !rids),npatt in let term2 = - GLetIn(dummy_loc,Anonymous, - GCast(dummy_loc,glob_of_pat npatt, - CastConv (DEFAULTcast,app_ind)),term1) in + GLetIn(Loc.ghost,Anonymous, + GCast(Loc.ghost,glob_of_pat npatt, + CastConv app_ind),term1) 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 + let constr = fst (understand env sigma term5)(*FIXME*) in let tparams,nam4,rest4 = match_args destProd [] constr params in let tpatvars,nam3,rest3 = match_args destProd nam4 rest4 loc_ids in let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in @@ -380,22 +382,22 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = pat_pat=patt; pat_expr=pat},thyps -let interp_cut interp_it sigma env cut= - let nenv,nstat = interp_it sigma env cut.cut_stat in +let interp_cut interp_it env sigma cut= + let nenv,nstat = interp_it env sigma cut.cut_stat in {cut with cut_stat=nstat; - cut_by=interp_justification_items sigma nenv cut.cut_by} + cut_by=interp_justification_items nenv sigma cut.cut_by} -let interp_no_bind interp_it sigma env x = - env,interp_it sigma env x +let interp_no_bind interp_it env sigma x = + env,interp_it env sigma x -let interp_suffices_clause sigma env (hyps,cot)= +let interp_suffices_clause env sigma (hyps,cot)= let (locvars,_) as res = match cot with This (c,_) -> - let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) sigma env hyps c in + let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) env sigma hyps c in nhyps,This nc - | Thesis Plain as th -> interp_hyps sigma env hyps,th + | Thesis Plain as th -> interp_hyps env sigma hyps,th | Thesis (For n) -> error "\"thesis for\" is not applicable here." in let push_one hyp env0 = match hyp with @@ -406,66 +408,66 @@ let interp_suffices_clause sigma env (hyps,cot)= 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) +let interp_casee env sigma = function + Real c -> Real (fst (understand env sigma (fst c)))(*FIXME*) + | Virtual cut -> Virtual (interp_cut (interp_no_bind (interp_statement (interp_constr true))) env sigma cut) let abstract_one_arg = function (loc,(id,None)) -> (fun glob -> - GLambda (dummy_loc,Name id, Explicit, - GHole (loc,Evd.BinderType (Name id)), glob)) + GLambda (Loc.ghost,Name id, Explicit, + GHole (loc,Evar_kinds.BinderType (Name id),Misctypes.IntroAnonymous,None), glob)) | (loc,(id,Some typ)) -> (fun glob -> - GLambda (dummy_loc,Name id, Explicit, fst typ, glob)) + GLambda (Loc.ghost,Name id, Explicit, fst typ, glob)) let glob_constr_of_fun args body = List.fold_right abstract_one_arg args (fst body) -let interp_fun sigma env args body = - let constr=understand sigma env (glob_constr_of_fun args body) in +let interp_fun env sigma args body = + let constr=fst (*FIXME*) (understand env sigma (glob_constr_of_fun args body)) in match_args destLambda [] constr args -let rec interp_bare_proof_instr info (sigma:Evd.evar_map) (env:Environ.env) = function - 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) +let rec interp_bare_proof_instr info env sigma = function + Pthus i -> Pthus (interp_bare_proof_instr info env sigma i) + | Pthen i -> Pthen (interp_bare_proof_instr info env sigma i) + | Phence i -> Phence (interp_bare_proof_instr info env sigma i) | Pcut c -> Pcut (interp_cut (interp_no_bind (interp_statement (interp_constr_or_thesis true))) - sigma env c) + env sigma c) | Psuffices c -> - Psuffices (interp_cut interp_suffices_clause sigma env c) + Psuffices (interp_cut interp_suffices_clause env sigma c) | Prew (s,c) -> Prew (s,interp_cut (interp_no_bind (interp_statement (interp_constr_in_type (get_eq_typ info env)))) - sigma env c) + env sigma c) - | Psuppose hyps -> Psuppose (interp_hyps sigma env hyps) + | Psuppose hyps -> Psuppose (interp_hyps env sigma hyps) | Pcase (params,pat,hyps) -> - let tparams,tpat,thyps = interp_cases info sigma env params pat hyps in + let tparams,tpat,thyps = interp_cases info env sigma params pat hyps in Pcase (tparams,tpat,thyps) | 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) - | Pper (et,c) -> Pper (et,interp_casee sigma env c) + Ptake (List.map (fun c -> fst (*FIXME*) (understand env sigma (fst c))) witl) + | Pconsider (c,hyps) -> Pconsider (interp_constr false env sigma c, + interp_hyps env sigma hyps) + | Pper (et,c) -> Pper (et,interp_casee env sigma c) | Pend bt -> Pend bt | Pescape -> Pescape - | Passume hyps -> Passume (interp_hyps sigma env hyps) - | Pgiven hyps -> Pgiven (interp_hyps sigma env hyps) - | 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) + | Passume hyps -> Passume (interp_hyps env sigma hyps) + | Pgiven hyps -> Pgiven (interp_hyps env sigma hyps) + | Plet hyps -> Plet (interp_hyps env sigma hyps) + | Pclaim st -> Pclaim (interp_statement (interp_constr true) env sigma st) + | Pfocus st -> Pfocus (interp_statement (interp_constr true) env sigma st) | Pdefine (id,args,body) -> - let nargs,_,nbody = interp_fun sigma env args body in + let nargs,_,nbody = interp_fun env sigma args body in Pdefine (id,nargs,nbody) | Pcast (id,typ) -> - Pcast(id,interp_constr true sigma env typ) + Pcast(id,interp_constr true env sigma typ) -let rec interp_proof_instr info sigma env instr= +let interp_proof_instr info env sigma instr= {emph = instr.emph; - instr = interp_bare_proof_instr info sigma env instr.instr} + instr = interp_bare_proof_instr info env sigma instr.instr} |