diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evd.ml | 68 | ||||
| -rw-r--r-- | proofs/evd.mli | 48 | ||||
| -rw-r--r-- | proofs/proof_trees.ml | 235 | ||||
| -rw-r--r-- | proofs/proof_trees.mli | 85 | ||||
| -rw-r--r-- | proofs/tmp-src | 148 |
5 files changed, 556 insertions, 28 deletions
diff --git a/proofs/evd.ml b/proofs/evd.ml new file mode 100644 index 0000000000..48b2a4b577 --- /dev/null +++ b/proofs/evd.ml @@ -0,0 +1,68 @@ + +(* $Id$ *) + +open Util +open Names +open Term +open Sign + +(* The type of mappings for existential variables *) + +type evar_body = + | Evar_empty + | Evar_defined of constr + +type 'a evar_info = { + evar_concl : typed_type; (* the type of the evar ... *) + evar_hyps : typed_type signature; (* ... under a certain signature *) + evar_body : evar_body; (* its definition *) + evar_info : 'a option } (* any other necessary information *) + +type 'a evar_map = 'a evar_info Spmap.t + +let mt_evd = Spmap.empty + +let toList evc = Spmap.fold (fun sp x acc -> (sp,x)::acc) evc [] +let dom evc = Spmap.fold (fun sp _ acc -> sp::acc) evc [] +let map evc k = Spmap.find k evc +let rmv evc k = Spmap.remove k evc +let remap evc k i = Spmap.add k i evc +let in_dom evc k = Spmap.mem k evc + +let add_with_info evd sp newinfo = + Spmap.add sp newinfo evd + +let add_noinfo evd sp sign typ = + let newinfo = + { evar_concl = typ; + evar_hyps = sign; + evar_body = Evar_empty; + evar_info = None} + in + Spmap.add sp newinfo evd + +let define evd sp body = + let oldinfo = map evd sp in + let newinfo = + { evar_concl = oldinfo.evar_concl; + evar_hyps = oldinfo.evar_hyps; + evar_body = Evar_defined body; + evar_info = oldinfo.evar_info} + in + match oldinfo.evar_body with + | Evar_empty -> Spmap.add sp newinfo evd + | _ -> anomaly "cannot define an isevar twice" + +(* The list of non-instantiated existential declarations *) + +let non_instantiated sigma = + let listsp = toList sigma in + List.fold_left + (fun l ((sp,evd) as d) -> + if evd.evar_body = Evar_empty then (d::l) else l) + [] listsp + +let is_evar sigma sp = in_dom sigma sp + +let is_defined sigma sp = + let info = map sigma sp in not (info.evar_body = Evar_empty) diff --git a/proofs/evd.mli b/proofs/evd.mli new file mode 100644 index 0000000000..8063f42b02 --- /dev/null +++ b/proofs/evd.mli @@ -0,0 +1,48 @@ + +(* $Id$ *) + +(*i*) +open Names +open Term +open Sign +(*i*) + +(* The type of mappings for existential variables. + The keys are section paths and the associated information is a record + containing the type of the evar ([concl]), the signature under which + it was introduced ([hyps]), its definition ([body]) and any other + possible information if necessary ([info]). +*) + +type evar_body = + | Evar_empty + | Evar_defined of constr + +type 'a evar_info = { + evar_concl : typed_type; + evar_hyps : typed_type signature; + evar_body : evar_body; + evar_info : 'a option } + +type 'a evar_map + +val dom : 'a evar_map -> section_path list +val map : 'a evar_map -> section_path -> 'a evar_info +val rmv : 'a evar_map -> section_path -> 'a evar_map +val remap : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map +val in_dom : 'a evar_map -> section_path -> bool +val toList : 'a evar_map -> (section_path * 'a evar_info) list + +val mt_evd : 'a evar_map +val add_with_info : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map +val add_noinfo : + 'a evar_map -> section_path -> typed_type signature -> typed_type + -> 'a evar_map + +val define : 'a evar_map -> section_path -> constr -> 'a evar_map + +val non_instantiated : 'a evar_map -> (section_path * 'a evar_info) list +val is_evar : 'a evar_map -> section_path -> bool + +val is_defined : 'a evar_map -> section_path -> bool + diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 77e8314d5f..4680607244 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -1,7 +1,11 @@ (* $Id$ *) +open Names open Term +open Sign +open Evd +open Stamps type bindOcc = | Dep of identifier @@ -11,20 +15,20 @@ type bindOcc = type 'a substitution = (bindOcc * 'a) list type tactic_arg = - | COMMAND of Coqast.t - | CONSTR of constr - | IDENTIFIER of identifier - | INTEGER of int - | CLAUSE of identifier list - | BINDINGS of Coqast.t substitution - | CBINDINGS of constr substitution - | QUOTED_STRING of string - | TACEXP of Coqast.t - | REDEXP of string * Coqast.t list - | FIXEXP of identifier * int * Coqast.t - | COFIXEXP of identifier * Coqast.t - | LETPATTERNS of int list option * (identifier * int list) list - | INTROPATTERN of intro_pattern + | Command of Coqast.t + | Constr of constr + | Identifier of identifier + | Integer of int + | Clause of identifier list + | Bindings of Coqast.t substitution + | Cbindings of constr substitution + | Quoted_string of string + | Tacexp of Coqast.t + | Redexp of string * Coqast.t list + | Fixexp of identifier * int * Coqast.t + | Cofixexp of identifier * Coqast.t + | Letpatterns of int list option * (identifier * int list) list + | Intropattern of intro_pattern and intro_pattern = | IdPat of identifier @@ -33,3 +37,206 @@ and intro_pattern = | ListPat of intro_pattern list and tactic_expression = string * tactic_arg list + + +type pf_status = Complete_proof | Incomplete_proof + +type prim_rule_name = + | Intro + | Intro_after + | Intro_replacing + | Fix + | Cofix + | Refine + | Convert_concl + | Convert_hyp + | Thin + | Move of bool + +type prim_rule = { + name : prim_rule_name; + hypspecs : identifier list; + newids : identifier list; + params : Coqast.t list; + terms : constr list } + +type local_constraints = Spset.t + +type proof_tree = { + status : pf_status; + goal : goal; + ref : (rule * proof_tree list) option; + subproof : proof_tree option } + +and goal = ctxtty evar_info + +and rule = + | Prim of prim_rule + | Tactic of tactic_expression + | Context of ctxtty + | Local_constraints of local_constraints + +and ctxtty = { + pgm : constr option; + mimick : proof_tree option; + lc : local_constraints } + +and evar_declarations = ctxtty evar_map + +let is_bind = function + | Bindings _ -> true + | _ -> false + +let lc_toList lc = Spset.elements lc + +(* Functions on goals *) + +let mkGOAL ctxt sign cl = + { evar_hyps = sign; + evar_concl = cl; + evar_body = Evar_empty; + evar_info = Some ctxt } + +(* Functions on the information associated with existential variables *) + +let mt_ctxt lc = { pgm = None; mimick = None; lc = lc } + +let get_ctxt ctxt = + match ctxt.evar_info with + | Some x -> x + | None -> assert false + +let get_pgm evd = + match evd.evar_info with + | Some x -> x.pgm + | None -> assert false + +let set_pgm pgm ctxt = { ctxt with pgm = pgm } + +let get_mimick evd = + match evd.evar_info with + | Some x -> x.mimick + | None -> assert false + +let set_mimick mimick ctxt = {mimick = mimick; pgm = ctxt.pgm;lc=ctxt.lc} + +let get_lc evd = + match evd.evar_info with + | Some x -> x.lc + | None -> assert false + +(* Functions on proof trees *) + +let ref_of_proof pf = + match pf.ref with + | None -> failwith "rule_of_proof" + | Some r -> r + +let rule_of_proof pf = + let (r,_) = ref_of_proof pf in r + +let children_of_proof pf = + let (_,cl) = ref_of_proof pf in cl + +let goal_of_proof pf = pf.goal + +let subproof_of_proof pf = + match pf.subproof with + | None -> failwith "subproof_of_proof" + | Some pf -> pf + +let status_of_proof pf = pf.status + +let is_complete_proof pf = pf.status = Complete_proof + +let is_leaf_proof pf = + match pf.ref with + | None -> true + | Some _ -> false + +let is_tactic_proof pf = + match pf.subproof with + | Some _ -> true + | None -> false + + +(*******************************************************************) +(* Constraints for existential variables *) +(*******************************************************************) + +(* A local constraint is just a set of section_paths *) + +(* recall : type local_constraints = Spset.t *) + +(* A global constraint is a mappings of existential variables + with some extra information for the program and mimick + tactics. *) + +type global_constraints = evar_declarations timestamped + +(* A readable constraint is a global constraint plus a focus set + of existential variables and a signature. *) + +type evar_recordty = { + focus : local_constraints; + sign : typed_type signature; + decls : evar_declarations } + +and readable_constraints = evar_recordty timestamped + +(* Functions on readable constraints *) + +let mt_evcty lc gc = + ts_mk { focus = lc; sign = nil_sign; decls = gc } + +let evc_of_evds evds gl = + ts_mk { focus = (get_lc gl); sign = gl.evar_hyps ; decls = evds } + +let rc_of_gc gc gl = evc_of_evds (ts_it gc) gl + +let rc_add evc (k,v) = + ts_mod + (fun evc -> { focus =(Spset.add k evc.focus); + sign = evc.sign; + decls = Evd.add_with_info evc.decls k v }) + evc + +let get_hyps evc = (ts_it evc).sign +let get_focus evc = (ts_it evc).focus +let get_decls evc = (ts_it evc).decls +let get_gc evc = (ts_mk (ts_it evc).decls) +let remap evc (k,v) = + ts_mod + (fun evc -> { focus = evc.focus; + sign = evc.sign; + decls = Evd.remap evc.decls k v }) + evc + +let lc_exists f lc = Spset.fold (fun e b -> (f e) or b) lc false + +(* MENTIONS SIGMA SP LOC is true exactly when LOC is defined, and SP is + * on LOC's access list, or an evar on LOC's access list mentions SP. *) + +let rec mentions sigma sp loc = + let loc_evd = map (ts_it sigma).decls loc in + match loc_evd.evar_body with + | Evar_defined _ -> (Spset.mem sp (get_lc loc_evd) + or lc_exists (mentions sigma sp) (get_lc loc_evd)) + | _ -> false + +(* ACCESSIBLE SIGMA SP LOC is true exactly when SP is on LOC's access list, + * or there exists a LOC' on LOC's access list such that + * MENTIONS SIGMA SP LOC' is true. *) + +let rec accessible sigma sp loc = + let loc_evd = map (ts_it sigma).decls loc in + lc_exists (fun loc' -> sp = loc' or mentions sigma sp loc') (get_lc loc_evd) + + +(* [ctxt_access sigma sp] is true when SIGMA is accessing a current + * accessibility list ACCL, and SP is either on ACCL, or is mentioned + * in the body of one of the ACCL. *) + +let ctxt_access sigma sp = + lc_exists (fun sp' -> sp' = sp or mentions sigma sp sp') (ts_it sigma).focus + diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index 99d94d01e3..38f7aeb8ec 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -4,8 +4,12 @@ (*i*) open Names open Term +open Evd (*i*) +(* This module declares the structure of proof trees, global and + readable constraints, and a few utilities on these types *) + type bindOcc = | Dep of identifier | NoDep of int @@ -14,20 +18,20 @@ type bindOcc = type 'a substitution = (bindOcc * 'a) list type tactic_arg = - | COMMAND of Coqast.t - | CONSTR of constr - | IDENTIFIER of identifier - | INTEGER of int - | CLAUSE of identifier list - | BINDINGS of Coqast.t substitution - | CBINDINGS of constr substitution - | QUOTED_STRING of string - | TACEXP of Coqast.t - | REDEXP of string * Coqast.t list - | FIXEXP of identifier * int * Coqast.t - | COFIXEXP of identifier * Coqast.t - | LETPATTERNS of int list option * (identifier * int list) list - | INTROPATTERN of intro_pattern + | Command of Coqast.t + | Constr of constr + | Identifier of identifier + | Integer of int + | Clause of identifier list + | Bindings of Coqast.t substitution + | Cbindings of constr substitution + | Quoted_string of string + | Tacexp of Coqast.t + | Redexp of string * Coqast.t list + | Fixexp of identifier * int * Coqast.t + | Cofixexp of identifier * Coqast.t + | Letpatterns of int list option * (identifier * int list) list + | Intropattern of intro_pattern and intro_pattern = | IdPat of identifier @@ -36,3 +40,56 @@ and intro_pattern = | ListPat of intro_pattern list and tactic_expression = string * tactic_arg list + + +type pf_status = Complete_proof | Incomplete_proof + +type prim_rule_name = + | Intro + | Intro_after + | Intro_replacing + | Fix + | Cofix + | Refine + | Convert_concl + | Convert_hyp + | Thin + | Move of bool + +type prim_rule = { + name : prim_rule_name; + hypspecs : identifier list; + newids : identifier list; + params : Coqast.t list; + terms : constr list } + +type local_constraints = Spset.t + +(* [ref] = [None] if the goal has still to be proved, + and [Some (r,l)] if the rule [r] was applied to the goal + and gave [l] as subproofs to be completed. + + [subproof] = [(Some p)] if [ref = (Some(Tactic t,l))]; + [p] is then the proof that the goal can be proven if the goals + in [l] are solved *) + +type proof_tree = { + status : pf_status; + goal : goal; + ref : (rule * proof_tree list) option; + subproof : proof_tree option } + +and goal = ctxtty evar_info + +and rule = + | Prim of prim_rule + | Tactic of tactic_expression + | Context of ctxtty + | Local_constraints of local_constraints + +and ctxtty = { + pgm : constr option; + mimick : proof_tree option; + lc : local_constraints } + +and evar_declarations = ctxtty evar_map diff --git a/proofs/tmp-src b/proofs/tmp-src new file mode 100644 index 0000000000..eca0119b18 --- /dev/null +++ b/proofs/tmp-src @@ -0,0 +1,148 @@ + +(********* INSTANTIATE ****************************************************) + +(* existential_type gives the type of an existential *) +let existential_type env k = + let (sp,args) = destConst k in + let evd = Evd.map (evar_map env) sp in + instantiate_constr + (ids_of_sign evd.evar_hyps) evd.evar_concl.body (Array.to_list args) + +(* existential_value gives the value of a defined existential *) +let existential_value env k = + let (sp,args) = destConst k in + if defined_const env k then + let evd = Evd.map (evar_map env) sp in + match evd.evar_body with + | EVAR_DEFINED c -> + instantiate_constr (ids_of_sign evd.evar_hyps) c (Array.to_list args) + | _ -> anomalylabstrm "termenv__existential_value" + [< 'sTR"The existential variable code just registered a" ; + 'sPC ; 'sTR"grave internal error." >] + else + failwith "undefined existential" + + +(******* REDUCTION ********************************************************) + +(* Expanding existential variables (trad.ml, progmach.ml) *) +(* 1- whd_ise fails if an existential is undefined *) +let rec whd_ise env = function + | DOPN(Const sp,_) as k -> + if Evd.in_dom (evar_map env) sp then + if defined_constant env k then + whd_ise env (constant_value env k) + else + errorlabstrm "whd_ise" + [< 'sTR"There is an unknown subterm I cannot solve" >] + else + k + | DOP2(Cast,c,_) -> whd_ise env c + | DOP0(Sort(Type(_))) -> DOP0(Sort(Type(dummy_univ))) + | c -> c + + +(* 2- undefined existentials are left unchanged *) +let rec whd_ise1 env = function + | (DOPN(Const sp,_) as k) -> + if Evd.in_dom (evar_map env) sp & defined_const env k then + whd_ise1 env (constant_value env k) + else + k + | DOP2(Cast,c,_) -> whd_ise1 env c + | DOP0(Sort(Type _)) -> DOP0(Sort(Type dummy_univ)) + | c -> c + +let nf_ise1 env = strong (whd_ise1 env) env + +(* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables + * Similarly we have is_fmachine1_metas and is_resolve1_metas *) + +let rec whd_ise1_metas env = function + | (DOPN(Const sp,_) as k) -> + if Evd.in_dom (evar_map env) sp then + if defined_const env k then + whd_ise1_metas env (const_or_ex_value env k) + else + let m = DOP0(Meta (new_meta())) in + DOP2(Cast,m,const_or_ex_type env k) + else + k + | DOP2(Cast,c,_) -> whd_ise1_metas env c + | c -> c + +(********************************************************************) +(* Special-Purpose Reduction *) +(********************************************************************) + +let whd_meta env = function + | DOP0(Meta p) as u -> (try List.assoc p (metamap env) with Not_found -> u) + | x -> x + +(* Try to replace all metas. Does not replace metas in the metas' values + * Differs from (strong whd_meta). *) +let plain_instance env c = + let s = metamap env in + let rec irec = function + | DOP0(Meta p) as u -> (try List.assoc p s with Not_found -> u) + | DOP1(oper,c) -> DOP1(oper, irec c) + | DOP2(oper,c1,c2) -> DOP2(oper, irec c1, irec c2) + | DOPN(oper,cl) -> DOPN(oper, Array.map irec cl) + | DOPL(oper,cl) -> DOPL(oper, List.map irec cl) + | DLAM(x,c) -> DLAM(x, irec c) + | DLAMV(x,v) -> DLAMV(x, Array.map irec v) + | u -> u + in + if s = [] then c else irec c + +(* Pourquoi ne fait-on pas nf_betaiota si s=[] ? *) +let instance env c = + let s = metamap env in + if s = [] then c else nf_betaiota env (plain_instance env c) + +(************ REDUCTION.MLI **********************************************) + +(*s Special-Purpose Reduction Functions *) +val whd_meta : 'a reduction_function +val plain_instance : 'a reduction_function +val instance : 'a reduction_function + +val whd_ise : 'a reduction_function +val whd_ise1 : 'a reduction_function +val nf_ise1 : 'a reduction_function +val whd_ise1_metas : 'a reduction_function + +(*********** TYPEOPS *****************************************************) + +(* Existentials. *) + +let type_of_existential env c = + let (sp,args) = destConst c in + let info = Evd.map (evar_map env) sp in + let hyps = info.evar_hyps in + check_hyps (basename sp) env hyps; + instantiate_type (ids_of_sign hyps) info.evar_concl (Array.to_list args) + +(* Constants or existentials. *) + +let type_of_constant_or_existential env c = + if is_existential c then + type_of_existential env c + else + type_of_constant env c + + +(******** TYPING **********************************************************) + + | IsMeta n -> + let metaty = + try lookup_meta n env + with Not_found -> error "A variable remains non instanciated" + in + (match kind_of_term metaty with + | IsCast (typ,kind) -> + ({ uj_val = cstr; uj_type = typ; uj_kind = kind }, cst0) + | _ -> + let (jty,cst) = execute mf env metaty in + let k = whd_betadeltaiotaeta env jty.uj_type in + ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, cst)) |