diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /contrib/funind/indfun_common.ml | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'contrib/funind/indfun_common.ml')
-rw-r--r-- | contrib/funind/indfun_common.ml | 319 |
1 files changed, 319 insertions, 0 deletions
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml new file mode 100644 index 00000000..b32dfacb --- /dev/null +++ b/contrib/funind/indfun_common.ml @@ -0,0 +1,319 @@ +open Names +open Pp + +open Libnames + +let mk_prefix pre id = id_of_string (pre^(string_of_id id)) +let mk_rel_id = mk_prefix "R_" + +let msgnl m = + () + +let invalid_argument s = raise (Invalid_argument s) + +(* let idtbl = Hashtbl.create 29 *) +(* let reset_name () = Hashtbl.clear idtbl *) + +(* let fresh_id s = *) +(* try *) +(* let id = Hashtbl.find idtbl s in *) +(* incr id; *) +(* id_of_string (s^(string_of_int !id)) *) +(* with Not_found -> *) +(* Hashtbl.add idtbl s (ref (-1)); *) +(* id_of_string s *) + +(* let fresh_name s = Name (fresh_id s) *) +(* let get_name ?(default="H") = function *) +(* | Anonymous -> fresh_name default *) +(* | Name n -> Name n *) + + + +let fresh_id avoid s = Termops.next_global_ident_away true (id_of_string s) avoid + +let fresh_name avoid s = Name (fresh_id avoid s) + +let get_name avoid ?(default="H") = function + | Anonymous -> fresh_name avoid default + | Name n -> Name n + +let array_get_start a = + try + Array.init + (Array.length a - 1) + (fun i -> a.(i)) + with Invalid_argument "index out of bounds" -> + invalid_argument "array_get_start" + +let id_of_name = function + Name id -> id + | _ -> raise Not_found + +let locate ref = + let (loc,qid) = qualid_of_reference ref in + Nametab.locate qid + +let locate_ind ref = + match locate ref with + | IndRef x -> x + | _ -> raise Not_found + +let locate_constant ref = + match locate ref with + | ConstRef x -> x + | _ -> raise Not_found + + +let locate_with_msg msg f x = + try + f x + with + | Not_found -> raise (Util.UserError("", msg)) + | e -> raise e + + +let filter_map filter f = + let rec it = function + | [] -> [] + | e::l -> + if filter e + then + (f e) :: it l + else it l + in + it + + +let chop_rlambda_n = + let rec chop_lambda_n acc n rt = + if n == 0 + then List.rev acc,rt + else + match rt with + | Rawterm.RLambda(_,name,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b + | Rawterm.RLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b + | _ -> + raise (Util.UserError("chop_rlambda_n", + str "chop_rlambda_n: Not enough Lambdas")) + in + chop_lambda_n [] + +let chop_rprod_n = + let rec chop_prod_n acc n rt = + if n == 0 + then List.rev acc,rt + else + match rt with + | Rawterm.RProd(_,name,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b + | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) + in + chop_prod_n [] + + + +let list_union_eq eq_fun l1 l2 = + let rec urec = function + | [] -> l2 + | a::l -> if List.exists (eq_fun a) l2 then urec l else a::urec l + in + urec l1 + +let list_add_set_eq eq_fun x l = + if List.exists (eq_fun x) l then l else x::l + + + + +let const_of_id id = + let _,princ_ref = + qualid_of_reference (Libnames.Ident (Util.dummy_loc,id)) + in + try Nametab.locate_constant princ_ref + with Not_found -> Util.error ("cannot find "^ string_of_id id) + +let def_of_const t = + match (Term.kind_of_term t) with + Term.Const sp -> + (try (match (Global.lookup_constant sp) with + {Declarations.const_body=Some c} -> Declarations.force c + |_ -> assert false) + with _ -> assert false) + |_ -> assert false + +let coq_constant s = + Coqlib.gen_constant_in_modules "RecursiveDefinition" + (Coqlib.init_modules @ Coqlib.arith_modules) s;; + +let constant sl s = + constr_of_reference + (Nametab.locate (make_qualid(Names.make_dirpath + (List.map id_of_string (List.rev sl))) + (id_of_string s)));; + +let find_reference sl s = + (Nametab.locate (make_qualid(Names.make_dirpath + (List.map id_of_string (List.rev sl))) + (id_of_string s)));; + +let eq = lazy(coq_constant "eq") +let refl_equal = lazy(coq_constant "refl_equal") + + +(* (\************************************************\) *) +(* (\* Should be removed latter *\) *) +(* (\* Comes from new induction (cf Pierre) *\) *) +(* (\************************************************\) *) + +(* open Sign *) +(* open Term *) + +(* type elim_scheme = *) + +(* (\* { (\\* lists are in reverse order! *\\) *\) *) +(* (\* params: rel_context; (\\* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *\\) *\) *) +(* (\* predicates: rel_context; (\\* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *\\) *\) *) +(* (\* branches: rel_context; (\\* branchr,...,branch1 *\\) *\) *) +(* (\* args: rel_context; (\\* (xni, Ti_ni) ... (x1, Ti_1) *\\) *\) *) +(* (\* indarg: rel_declaration option; (\\* Some (H,I prm1..prmp x1...xni) if present, None otherwise *\\) *\) *) +(* (\* concl: types; (\\* Qi x1...xni HI, some prmis may not be present *\\) *\) *) +(* (\* indarg_in_concl:bool; (\\* true if HI appears at the end of conclusion (dependent scheme) *\\) *\) *) +(* (\* } *\) *) + + + +(* let occur_rel n c = *) +(* let res = not (noccurn n c) in *) +(* res *) + +(* let list_filter_firsts f l = *) +(* let rec list_filter_firsts_aux f acc l = *) +(* match l with *) +(* | e::l' when f e -> list_filter_firsts_aux f (acc@[e]) l' *) +(* | _ -> acc,l *) +(* in *) +(* list_filter_firsts_aux f [] l *) + +(* let count_rels_from n c = *) +(* let rels = Termops.free_rels c in *) +(* let cpt,rg = ref 0, ref n in *) +(* while Util.Intset.mem !rg rels do *) +(* cpt:= !cpt+1; rg:= !rg+1; *) +(* done; *) +(* !cpt *) + +(* let count_nonfree_rels_from n c = *) +(* let rels = Termops.free_rels c in *) +(* if Util.Intset.exists (fun x -> x >= n) rels then *) +(* let cpt,rg = ref 0, ref n in *) +(* while not (Util.Intset.mem !rg rels) do *) +(* cpt:= !cpt+1; rg:= !rg+1; *) +(* done; *) +(* !cpt *) +(* else raise Not_found *) + +(* (\* cuts a list in two parts, first of size n. Size must be greater than n *\) *) +(* let cut_list n l = *) +(* let rec cut_list_aux acc n l = *) +(* if n<=0 then acc,l *) +(* else match l with *) +(* | [] -> assert false *) +(* | e::l' -> cut_list_aux (acc@[e]) (n-1) l' in *) +(* let res = cut_list_aux [] n l in *) +(* res *) + +(* let exchange_hd_prod subst_hd t = *) +(* let hd,args= decompose_app t in mkApp (subst_hd,Array.of_list args) *) + +(* let compute_elim_sig elimt = *) +(* (\* conclusion is the final (Qi ...) *\) *) +(* let hyps,conclusion = decompose_prod_assum elimt in *) +(* (\* ccl is conclusion where Qi (that is rel <something>) is replaced *) +(* by a constant (Prop) to avoid it being counted as an arg or *) +(* parameter in the following. *\) *) +(* let ccl = exchange_hd_prod mkProp conclusion in *) +(* (\* indarg is the inductive argument if it exists. If it exists it is *) +(* the last hyp before the conclusion, so it is the first element of *) +(* hyps. To know the first elmt is an inductive arg, we check if the *) +(* it appears in the conclusion (as rel 1). If yes, then it is not *) +(* an inductive arg, otherwise it is. There is a pathological case *) +(* with False_inf where Qi is rel 1, so we first get rid of Qi in *) +(* ccl. *\) *) +(* (\* if last arg of ccl is an application then this a functional ind *) +(* principle *\) let last_arg_ccl = *) +(* try List.hd (List.rev (snd (decompose_app ccl))) *) +(* with Failure "hd" -> mkProp in (\* dummy constr that is not an app *) +(* *\) let hyps',indarg,dep = *) +(* if isApp last_arg_ccl *) +(* then *) +(* hyps,None , false (\* no HI at all *\) *) +(* else *) +(* try *) +(* if noccurn 1 ccl (\* rel 1 does not occur in ccl *\) *) +(* then *) +(* List.tl hyps , Some (List.hd hyps), false (\* it does not *) +(* occur in concl *\) else *) +(* List.tl hyps , Some (List.hd hyps) , true (\* it does occur in concl *\) *) +(* with Failure s -> Util.error "cannot recognise an induction schema" *) +(* in *) + +(* (\* Arguments [xni...x1] must appear in the conclusion, so we count *) +(* successive rels appearing in conclusion **Qi is not considered a *) +(* rel** *\) let nargs = count_rels_from *) +(* (match indarg with *) +(* | None -> 1 *) +(* | Some _ -> 2) ccl in *) +(* let args,hyps'' = cut_list nargs hyps' in *) +(* let rel_is_pred (_,_,c) = isSort (snd(decompose_prod_assum c)) in *) +(* let branches,hyps''' = *) +(* list_filter_firsts (function x -> not (rel_is_pred x)) hyps'' *) +(* in *) +(* (\* Now we want to know which hyps remaining are predicates and which *) +(* are parameters *\) *) +(* (\* We rebuild *) + +(* forall (x1:Ti_1) (xni:Ti_ni) (HI:I prm1..prmp x1...xni), DUMMY *) +(* x1...xni HI ^^^^^^^^^^^^^^^^^^^^^^^^^ ^^ *) +(* optional *) +(* opt *) + +(* Free rels appearing in this term are parameters. We catch all of *) +(* them if HI is present. In this case the number of parameters is *) +(* the number of free rels. Otherwise (principle generated by *) +(* functional induction or by hand) WE GUESS that all parameters *) +(* appear in Ti_js, IS THAT TRUE??. *) + +(* TODO: if we want to generalize to the case where arges are merged *) +(* with branches (?) and/or where several predicates are cited in *) +(* the conclusion, we should do something more precise than just *) +(* counting free rels. *) +(* *\) *) +(* let concl_with_indarg = *) +(* match indarg with *) +(* | None -> ccl *) +(* | Some c -> it_mkProd_or_LetIn ccl [c] in *) +(* let concl_with_args = it_mkProd_or_LetIn concl_with_indarg args in *) +(* (\* let nparams2 = Util.Intset.cardinal (Termops.free_rels concl_with_args) in *\) *) +(* let nparams = *) +(* try List.length (hyps'''@branches) - count_nonfree_rels_from 1 *) +(* concl_with_args with Not_found -> 0 in *) +(* let preds,params = cut_list (List.length hyps''' - nparams) hyps''' in *) +(* let elimscheme = { *) +(* params = params; *) +(* predicates = preds; *) +(* branches = branches; *) +(* args = args; *) +(* indarg = indarg; *) +(* concl = conclusion; *) +(* indarg_in_concl = dep; *) +(* } *) +(* in *) +(* elimscheme *) + +(* let get_params elimt = *) +(* (compute_elim_sig elimt).params *) +(* (\************************************************\) *) +(* (\* end of Should be removed latter *\) *) +(* (\* Comes from new induction (cf Pierre) *\) *) +(* (\************************************************\) *) + |