diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /contrib/subtac/eterm.ml | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'contrib/subtac/eterm.ml')
-rw-r--r-- | contrib/subtac/eterm.ml | 148 |
1 files changed, 78 insertions, 70 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 859f9013..790e61a0 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -32,47 +32,48 @@ let list_assoc_index x l = | [] -> raise Not_found in aux 0 l + (** Substitute evar references in t using De Bruijn indices, where n binders were passed through. *) -let subst_evars evs n t = +let subst_evar_constr evs n t = + let seen = ref Intset.empty in let evar_info id = let rec aux i = function - (k, h, v) :: tl -> - trace (str "Searching for " ++ int id ++ str " found: " ++ int k); - if k = id then (i, h, v) else aux (succ i) tl + (k, x) :: tl -> + if k = id then x else aux (succ i) tl | [] -> raise Not_found - in - let (idx, hyps, v) = aux 0 evs in - n + idx + 1, hyps + in aux 0 evs in let rec substrec depth c = match kind_of_term c with | Evar (k, args) -> - (let index, hyps = - try evar_info k - with Not_found -> - anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found") - in - (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++ - int (List.length hyps) ++ str " hypotheses"); with _ -> () ); - let ex = mkRel (index + depth) in - (* Evar arguments are created in inverse order, - and we must not apply to defined ones (i.e. LetIn's) - *) - let args = - let rec aux hyps args acc = + let (id, idstr), hyps, _, _ = + try evar_info k + with Not_found -> + anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found") + in + seen := Intset.add id !seen; + (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++ + int (List.length hyps) ++ str " hypotheses"); with _ -> () ); + (* Evar arguments are created in inverse order, + and we must not apply to defined ones (i.e. LetIn's) + *) + let args = + let rec aux hyps args acc = match hyps, args with ((_, None, _) :: tlh), (c :: tla) -> aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc) | ((_, Some _, _) :: tlh), (_ :: tla) -> aux tlh tla acc | [], [] -> acc - | _, _ -> failwith "subst_evars: invalid argument" + | _, _ -> acc (*failwith "subst_evars: invalid argument"*) in aux hyps (Array.to_list args) [] in - mkApp (ex, Array.of_list args)) + mkApp (mkVar idstr, Array.of_list args) | _ -> map_constr_with_binders succ substrec depth c in - substrec 0 t + let t' = substrec 0 t in + t', !seen + (** Substitute variable references in t using De Bruijn indices, where n binders were passed through. *) @@ -89,73 +90,80 @@ let subst_vars acc n t = (** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ]) to a product : forall H1 : t1, ..., forall Hn : tn, concl. - Changes evars and hypothesis references to De Bruijn indices. + Changes evars and hypothesis references to variable references. *) let etype_of_evar evs ev hyps = let rec aux acc n = function (id, copt, t) :: tl -> - let t' = subst_evars evs n t in + let t', s = subst_evar_constr evs n t in let t'' = subst_vars acc 0 t' in - mkNamedProd_or_LetIn (id, copt, t'') (aux (id :: acc) (succ n) tl) + let copt', s = + match copt with + Some c -> + let c', s' = subst_evar_constr evs n c in + Some c', Intset.union s s' + | None -> None, s + in + let copt' = option_map (subst_vars acc 0) copt' in + let rest, s' = aux (id :: acc) (succ n) tl in + mkNamedProd_or_LetIn (id, copt', t'') rest, Intset.union s' s | [] -> - let t' = subst_evars evs n ev.evar_concl in - subst_vars acc 0 t' + let t', s = subst_evar_constr evs n ev.evar_concl in + subst_vars acc 0 t', s in aux [] 0 (rev hyps) open Tacticals -let eterm_term evm t tycon = +let rec take n l = + if n = 0 then [] else List.hd l :: take (pred n) (List.tl l) + +let trunc_named_context n ctx = + let len = List.length ctx in + take (len - n) ctx + +let eterm_obligations name nclen evm t tycon = (* 'Serialize' the evars, we assume that the types of the existentials refer to previous existentials in the list only *) let evl = List.rev (to_list evm) in - trace (str "Eterm, transformed to list"); + trace (str "Eterm, transformed to list"); + let evn = + let i = ref (-1) in + List.rev_map (fun (id, ev) -> incr i; + (id, (!i, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))), ev)) evl + in let evts = (* Remove existential variables in types and build the corresponding products *) fold_right - (fun (id, ev) l -> + (fun (id, (n, nstr), ev) l -> trace (str "Eterm: " ++ str "treating evar: " ++ int id); let hyps = Environ.named_context_of_val ev.evar_hyps in - let y' = (id, hyps, etype_of_evar l ev hyps) in + let hyps = trunc_named_context nclen hyps in + trace (str "Named context is: " ++ Printer.pr_named_context (Global.env ()) hyps); + let evtyp, deps = etype_of_evar l ev hyps in + trace (str "Evar " ++ str (string_of_int n) ++ str "'s type is: " ++ Termops.print_constr_env (Global.env ()) evtyp); + let y' = (id, ((n, nstr), hyps, evtyp, deps)) in y' :: l) - evl [] + evn [] in - let t' = (* Substitute evar refs in the term by De Bruijn indices *) - subst_evars evts 0 t - in - let evar_names = - List.map (fun (id, _, c) -> (id_of_string ("Evar" ^ string_of_int id)), c) evts - in - let evar_bl = - List.map (fun (id, c) -> Name id, None, c) evar_names - in - let anon_evar_bl = List.map (fun (_, x, y) -> (Anonymous, x, y)) evar_bl in - (* Generalize over the existential variables *) - let t'' = Termops.it_mkLambda_or_LetIn t' evar_bl - and tycon = option_map - (fun typ -> Termops.it_mkProd_wo_LetIn typ anon_evar_bl) tycon - in - let _declare_evar (id, c) = - let id = id_of_string ("Evar" ^ string_of_int id) in - ignore(Declare.declare_variable id (Names.empty_dirpath, Declare.SectionLocalAssum c, - Decl_kinds.IsAssumption Decl_kinds.Definitional)) + let t', _ = (* Substitute evar refs in the term by variables *) + subst_evar_constr evts 0 t in - let _declare_assert acc (id, c) = - let id = id_of_string ("Evar" ^ string_of_int id) in - tclTHEN acc (Tactics.assert_tac false (Name id) c) + let evars = + List.map (fun (_, ((_, name), _, typ, deps)) -> name, typ, deps) evts in (try trace (str "Term given to eterm" ++ spc () ++ - Termops.print_constr_env (Global.env ()) t); + Termops.print_constr_env (Global.env ()) t); trace (str "Term constructed in eterm" ++ spc () ++ - Termops.print_constr_env (Global.env ()) t''); - ignore(option_map - (fun typ -> - trace (str "Type :" ++ spc () ++ - Termops.print_constr_env (Global.env ()) typ)) - tycon); + Termops.print_constr_env (Global.env ()) t'); + ignore(iter + (fun (name, typ, deps) -> + trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++ + Termops.print_constr_env (Global.env ()) typ)) + evars); with _ -> ()); - t'', tycon, evar_names + Array.of_list (List.rev evars), t' let mkMetas n = let rec aux i acc = @@ -163,12 +171,12 @@ let mkMetas n = else acc in aux n [] -let eterm evm t (tycon : types option) = - let t, tycon, evs = eterm_term evm t tycon in - match tycon with - Some typ -> Tactics.apply_term (mkCast (t, DEFAULTcast, typ)) [] - | None -> Tactics.apply_term t (mkMetas (List.length evs)) +(* let eterm evm t (tycon : types option) = *) +(* let t, tycon, evs = eterm_term evm t tycon in *) +(* match tycon with *) +(* Some typ -> Tactics.apply_term (mkCast (t, DEFAULTcast, typ)) [] *) +(* | None -> Tactics.apply_term t (mkMetas (List.length evs)) *) -open Tacmach +(* open Tacmach *) -let etermtac (evm, t) = eterm evm t None +let etermtac (evm, t) = assert(false) (*eterm evm t None *) |