proceduralTypes.cmx: proceduralHelpers.cmx proceduralTypes.cmi
proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi
proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi
-proceduralConversion.cmo: proceduralConversion.cmi
-proceduralConversion.cmx: proceduralConversion.cmi
+proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi
+proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi
acic2Procedural.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi
acic2Procedural.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
proceduralTypes.cmx: proceduralHelpers.cmx proceduralTypes.cmi
proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi
proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi
-proceduralConversion.cmo: proceduralConversion.cmi
-proceduralConversion.cmx: proceduralConversion.cmi
+proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi
+proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi
acic2Procedural.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi
acic2Procedural.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
with Not_found -> `Type (CicUniv.fresh())
with Invalid_argument _ -> failwith "A2P.get_sort"
*)
-let get_type msg st bo =
-try
- let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.oblivion_ugraph in
- ty
-with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
-
let get_entry st id =
let rec aux = function
| [] -> assert false
in
aux st.context
-let get_ind_names uri tno =
-try
- let ts = match E.get_obj Un.oblivion_ugraph uri with
- | C.InductiveDefinition (ts, _, _, _), _ -> ts
- | _ -> assert false
- in
- match List.nth ts tno with
- | (_, _, _, cs) -> List.map fst cs
-with Invalid_argument _ -> failwith "A2P.get_ind_names"
-
let string_of_atomic = function
| C.ARel (_, _, _, s) -> s
| C.AVar (_, uri, _) -> H.name_of_uri uri None None
let names, _ = List.fold_left map ([], 1) l in
List.rev names
+let get_type msg st t = H.get_type msg st.context (H.cic t)
+
(* proof construction *******************************************************)
let anonymous_premise = C.Name "PREMISE"
let classes2, tl2, _, where = split2_last classes tl in
let script2 = List.rev (mk_arg st where) @ script in
let synth2 = I.S.add 1 synth in
- let names = get_ind_names uri tyno in
+ let names = H.get_ind_names uri tyno in
let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in
if List.length qs <> List.length names then
let qs = proc_bkd_proofs (next st) synth [] classes tl in
module C = Cic
module E = CicEnvironment
module Un = CicUniv
-module TC = CicTypeChecker
-module D = Deannotate
+module TC = CicTypeChecker
module UM = UriManager
module Rd = CicReduction
module PEH = ProofEngineHelpers
module PT = PrimitiveTactics
-
module DTI = DoubleTypeInference
-(* helpers ******************************************************************)
+module H = ProceduralHelpers
-let cic = D.deannotate_term
+(* helpers ******************************************************************)
let rec list_sub start length = function
| _ :: tl when start > 0 -> list_sub (pred start) length tl
| C.ALambda (_, _, _, t) when n > 0 ->
aux 0 (pred n) (lift 1 (-1) t)
| t when n > 0 ->
- Printf.eprintf "CLEAR: %u %s\n" n (CicPp.ppterm (cic t));
+ Printf.eprintf "CLEAR: %u %s\n" n (CicPp.ppterm (H.cic t));
assert false
| t -> t
in
aux [] c
let elim_inferred_type context goal arg using cpattern =
- let metasenv, ugraph = [], Un.oblivion_ugraph in
- let ety, _ugraph = TC.type_of_aux' metasenv context using ugraph in
+ let metasenv, ugraph = [], Un.default_ugraph in
+ let ety = H.get_type "elim_inferred_type" context using in
let _splits, args_no = PEH.split_with_whd (context, ety) in
let _metasenv, predicate, _arg, actual_args = PT.mk_predicate_for_elim
~context ~metasenv ~ugraph ~goal ~arg ~using ~cpattern ~args_no
module PER = ProofEngineReduction
module Ut = CicUtil
+(* raw cic prettyprinter ****************************************************)
+
+let xiter out so ss sc map l =
+ let rec aux = function
+ | hd :: tl when tl <> [] -> map hd; out ss; aux tl
+ | hd :: tl -> map hd; aux tl
+ | [] -> ()
+ in
+ out so; aux l; out sc
+
+let abst s w = Some (s, C.Decl w)
+
+let abbr s v w = Some (s, C.Def (v, w))
+
+let pp_sort out = function
+ | C.Type _ -> out "\Type"
+ | C.Prop -> out "\Prop"
+ | C.CProp _ -> out "\CProp"
+ | C.Set -> out "\Set"
+
+let pp_name out = function
+ | C.Name s -> out s
+ | C.Anonymous -> out "_"
+
+let pp_rel out c i =
+ try match List.nth c (pred i) with
+ | None -> out (Printf.sprintf "%u[?]" i)
+ | Some (s, _) -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
+ with Failure "nth" -> out (Printf.sprintf "%u[%u]" i (List.length c - i))
+
+let pp_implict out = function
+ | None -> out "?"
+ | Some `Closed -> out "?[Closed]"
+ | Some `Type -> out "?[Type]"
+ | Some `Hole -> out "?[Hole]"
+
+let pp_uri out a =
+ out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a))
+
+let rec pp_term out e c = function
+ | C.Sort h -> pp_sort out h
+ | C.Rel i -> pp_rel out c i
+ | C.Implicit x -> pp_implict out x
+ | C.Meta (i, iss) ->
+ let map = function None -> out "_" | Some v -> pp_term out e c v in
+ out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss
+ | C.Var (a, xss) ->
+ pp_uri out a; pp_xss out e c xss
+ | C.Const (a, xss) ->
+ pp_uri out a; pp_xss out e c xss
+ | C.MutInd (a, m, xss) ->
+ pp_uri out a; out (Printf.sprintf "/%u" m);
+ pp_xss out e c xss
+ | C.MutConstruct (a, m, n, xss) ->
+ pp_uri out a; out (Printf.sprintf "/%u/%u" m n);
+ pp_xss out e c xss
+ | C.Cast (v, w) ->
+ out "type "; pp_term out e c w; out " contains "; pp_term out e c v
+ | C.Appl vs ->
+ xiter out "(" " @ " ")" (pp_term out e c) vs
+ | C.MutCase (a, m, w, v, vs) ->
+ out "match "; pp_term out e c v;
+ out " of "; pp_uri out a; out (Printf.sprintf "/%u" m);
+ out " to "; pp_term out e c w;
+ xiter out " cases " " | " "" (pp_term out e c) vs
+ | C.Prod (s, w, t) ->
+ out "forall "; pp_name out s; out " of "; pp_term out e c w;
+ out " in "; pp_term out e (abst s w :: c) t
+ | C.Lambda (s, w, t) ->
+ out "fun "; pp_name out s; out " of "; pp_term out e c w;
+ out " in "; pp_term out e (abst s w :: c) t
+ | C.LetIn (s, v, w, t) ->
+ out "let "; pp_name out s;
+ out " def "; pp_term out e c v; out " of "; pp_term out e c w;
+ out " in "; pp_term out e (abbr s v w :: c) t
+ | C.Fix (i, fs) ->
+ let map c (s, _, w, v) = abbr (C.Name s) v w :: c in
+ let c' = List.fold_left map c fs in
+ let map (s, i, w, v) =
+ out (Printf.sprintf "%s[%u] def " s i); pp_term out e c' v;
+ out " of "; pp_term out e c w;
+ in
+ xiter out "let rec " " and " " in " map fs; pp_rel out c' (succ i)
+ | C.CoFix (i, fs) ->
+ let map c (s, w, v) = abbr (C.Name s) v w :: c in
+ let c' = List.fold_left map c fs in
+ let map (s, w, v) =
+ out s; pp_term out e c' v;
+ out " of "; pp_term out e c w;
+ in
+ xiter out "let corec " " and " " in " map fs; pp_rel out c' (succ i)
+
+and pp_xss out e c xss =
+ let map (a, v) = pp_uri out a; out " <- "; pp_term out e c v in
+ xiter out "[" "; " "]" map xss
+
(* fresh name generator *****************************************************)
let split name =
let fst3 (x, _, _) = x
let refine c t =
- try let t, _, _, _ = Rf.type_of_aux' [] c t Un.oblivion_ugraph in t
+ try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t
with e ->
Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
Printf.eprintf "Ref: term : %s\n" (Pp.ppterm t);
raise e
-let get_type c t =
- try let ty, _ = TC.type_of_aux' [] c t Un.oblivion_ugraph in ty
- with e ->
- Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
- Printf.eprintf "TC: term : %s\n" (Pp.ppterm t);
- raise e
+let get_type msg c t =
+ let log s =
+ prerr_endline ("TC: " ^ s);
+ prerr_endline ("TC: context: " ^ Pp.ppcontext c);
+ prerr_string "TC: term : "; pp_term prerr_string [] c t;
+ prerr_newline (); prerr_endline ("TC: location: " ^ msg)
+ in
+ try let ty, _ = TC.type_of_aux' [] c t Un.default_ugraph in ty with
+ | TC.TypeCheckerFailure s as e ->
+ log ("failure: " ^ Lazy.force s); raise e
+ | TC.AssertFailure s as e ->
+ log ("assert : " ^ Lazy.force s); raise e
let get_tail c t =
match PEH.split_with_whd (c, t) with
| _ -> assert false
let is_proof c t =
- match get_tail c (get_type c (get_type c t)) with
+ match get_tail c (get_type "is_proof 1" c (get_type "is_proof 2" c t)) with
| C.Sort C.Prop -> true
| C.Sort _ -> false
| _ -> assert false
let is_atomic t = not (is_not_atomic t)
let get_ind_type uri tyno =
- match E.get_obj Un.oblivion_ugraph uri with
+ match E.get_obj Un.default_ugraph uri with
| C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
| _ -> assert false
+let get_ind_names uri tno =
+try
+ let ts = match E.get_obj Un.default_ugraph uri with
+ | C.InductiveDefinition (ts, _, _, _), _ -> ts
+ | _ -> assert false
+ in
+ match List.nth ts tno with
+ | (_, _, _, cs) -> List.map fst cs
+with Invalid_argument _ -> failwith "get_ind_names"
+
let get_default_eliminator context uri tyno ty =
let _, (name, _, _, _) = get_ind_type uri tyno in
- let ext = match get_tail context (get_type context ty) with
+ let ext = match get_tail context (get_type "get_def_elim" context ty) with
| C.Sort C.Prop -> "_ind"
| C.Sort C.Set -> "_rec"
| C.Sort (C.CProp _) -> "_rect"
C.Const (uri, [])
let get_ind_parameters c t =
- let ty = get_type c t in
+ let ty = get_type "get_ind_pars 1" c t in
let ps = match get_tail c ty with
| C.MutInd _ -> []
| C.Appl (C.MutInd _ :: args) -> args
| _ -> assert false
in
- let disp = match get_tail c (get_type c ty) with
+ let disp = match get_tail c (get_type "get_ind_pars 2" c ty) with
| C.Sort C.Prop -> 0
| C.Sort _ -> 1
| _ -> assert false
let get_ind_type tys tyno =
let s, _, _, cs = List.nth tys tyno in s, cs
in
- match (fst (E.get_obj Un.oblivion_ugraph uri)), tyno, cno with
+ match (fst (E.get_obj Un.default_ugraph uri)), tyno, cno with
| C.Variable (s, _, _, _, _), _, _ -> s
| C.Constant (s, _, _, _, _), _, _ -> s
| C.InductiveDefinition (tys, _, _, _), Some i, None ->
* http://cs.unibo.it/helm/.
*)
+val pp_term:
+ (string -> unit) -> Cic.metasenv -> Cic.context -> Cic.term -> unit
val mk_fresh_name:
Cic.context -> Cic.name -> Cic.name
val list_map_cps:
val refine:
Cic.context -> Cic.term -> Cic.term
val get_type:
- Cic.context -> Cic.term -> Cic.term
+ string -> Cic.context -> Cic.term -> Cic.term
val is_proof:
Cic.context -> Cic.term -> bool
val is_sort:
Cic.term -> bool
val get_ind_type:
UriManager.uri -> int -> int * Cic.inductiveType
+val get_ind_names:
+ UriManager.uri -> int -> string list
val get_default_eliminator:
Cic.context -> UriManager.uri -> int -> Cic.term -> Cic.term
val get_ind_parameters:
* http://cs.unibo.it/helm/.
*)
+module UM = UriManager
module C = Cic
module Pp = CicPp
module I = CicInspect
+module E = CicEnvironment
module S = CicSubstitution
module DTI = DoubleTypeInference
module HEL = HExtlib
let defined_premise = "DEFINED"
-let get_type msg c bo =
-try
- let ty, _ = TC.type_of_aux' [] c bo Un.oblivion_ugraph in
- ty
-with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
-
let define c v =
let name = C.Name defined_premise in
- let ty = get_type "define" c v in
+ let ty = H.get_type "define" c v in
C.LetIn (name, v, ty, C.Rel 1)
let clear_absts m =
let g = function
| C.LetIn (nname, vv, ww, tt) when H.is_proof c v ->
let eentry = Some (nname, C.Def (vv, ww)) in
- let ttw = get_type "opt1_letin 1" (eentry :: c) tt in
+ let ttw = H.get_type "opt1_letin 1" (eentry :: c) tt in
let x = C.LetIn (nname, vv, ww,
C.LetIn (name, tt, ttw, S.lift_from 2 1 t)) in
HLog.warn "Optimizer: swap 1"; opt1_proof g true c x
HLog.warn "Optimizer: swap 2"; opt1_proof g true c x
| C.Lambda (name, ww, tt) ->
let v, vs = List.hd vs, List.tl vs in
- let w = get_type "opt1_appl 1" c v in
+ let w = H.get_type "opt1_appl 1" c v in
let x = C.Appl (C.LetIn (name, v, w, tt) :: vs) in
HLog.warn "Optimizer: remove 2"; opt1_proof g true c x
| C.Appl vvs ->
| _, [] -> assert false
in
let h () =
- let classes, conclusion = Cl.classify c (H.get_type c t) in
+ let classes, conclusion = Cl.classify c (H.get_type "opt1_appl 3" c t) in
let csno, vsno = List.length classes, List.length vs in
if csno < vsno then
let vvs, vs = HEL.split_nth csno vs in
let prev = List.map (S.lift 1) prev in
let vs = List.map (S.lift 1) vs in
let y = C.Appl (t :: List.rev prev @ tt :: vs) in
- let ww = get_type "opt1_appl 2" c vv in
+ let ww = H.get_type "opt1_appl 2" c vv in
let x = C.LetIn (name, vv, ww, y) in
HLog.warn "Optimizer: swap 3"; opt1_proof g true c x
| v :: vs -> aux h (v :: prev) vs
let g vs =
let x = C.Appl (t :: vs) in
let vsno = List.length vs in
- let _, csno = PEH.split_with_whd (c, H.get_type c t) in
+ let _, csno = PEH.split_with_whd (c, H.get_type "opt2_appl 1" c t) in
if vsno < csno then
- let tys, _ = PEH.split_with_whd (c, H.get_type c x) in
+ let tys, _ = PEH.split_with_whd (c, H.get_type "opt2_appl 2" c x) in
let tys = List.rev (List.tl tys) in
let tys, _ = HEL.split_nth (csno - vsno) tys in
HLog.warn "Optimizer: eta 1"; eta_expand g tys x
H.list_map_cps g (fun h -> opt2_term h c) vs
and opt2_other g c t =
- let tys, csno = PEH.split_with_whd (c, H.get_type c t) in
+ let tys, csno = PEH.split_with_whd (c, H.get_type "opt2_other" c t) in
if csno > 0 then begin
let tys = List.rev (List.tl tys) in
HLog.warn "Optimizer: eta 2"; eta_expand g tys t
let g bo =
Printf.eprintf "Optimized : %s\nPost Nodes: %u\n"
(Pp.ppterm bo) (I.count_nodes 0 bo);
- let _ = H.get_type [] (C.Cast (bo, ty)) in
+ prerr_string "H.pp_term : ";
+ H.pp_term prerr_string [] [] bo; prerr_newline ();
+ let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in
C.Constant (name, Some bo, ty, pars, attrs)
in
Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n"
name (I.count_nodes 0 bo);
- begin try opt1_term g (* (opt2_term g []) *) true [] bo
- with e -> failwith ("PPP: " ^ Printexc.to_string e) end
+ begin try opt1_term g (* (opt2_term g []) *) true [] bo with
+ | E.Object_not_found uri ->
+ let msg = "optimize_obj: object not found: " ^ UM.string_of_uri uri in
+ failwith msg
+ | e ->
+ let msg = "optimize_obj: " ^ Printexc.to_string e in
+ failwith msg
+ end
| obj -> obj
cicInspect.cmi: cic.cmo
cic.cmo: cicUniv.cmi
cic.cmx: cicUniv.cmx
-unshare.cmo: cic.cmo unshare.cmi
-unshare.cmx: cic.cmx unshare.cmi
cicUniv.cmo: cicUniv.cmi
cicUniv.cmx: cicUniv.cmi
-deannotate.cmo: cic.cmo deannotate.cmi
-deannotate.cmx: cic.cmx deannotate.cmi
+unshare.cmo: cicUniv.cmi cic.cmo unshare.cmi
+unshare.cmx: cicUniv.cmx cic.cmx unshare.cmi
+deannotate.cmo: unshare.cmi cic.cmo deannotate.cmi
+deannotate.cmx: unshare.cmx cic.cmx deannotate.cmi
cicParser.cmo: deannotate.cmi cicUniv.cmi cic.cmo cicParser.cmi
cicParser.cmx: deannotate.cmx cicUniv.cmx cic.cmx cicParser.cmi
cicUtil.cmo: cicUniv.cmi cic.cmo cicUtil.cmi
cicInspect.cmi: cic.cmx
cic.cmo: cicUniv.cmi
cic.cmx: cicUniv.cmx
-unshare.cmo: cic.cmx unshare.cmi
-unshare.cmx: cic.cmx unshare.cmi
cicUniv.cmo: cicUniv.cmi
cicUniv.cmx: cicUniv.cmi
-deannotate.cmo: cic.cmx deannotate.cmi
-deannotate.cmx: cic.cmx deannotate.cmi
+unshare.cmo: cicUniv.cmi cic.cmx unshare.cmi
+unshare.cmx: cicUniv.cmx cic.cmx unshare.cmi
+deannotate.cmo: unshare.cmi cic.cmx deannotate.cmi
+deannotate.cmx: unshare.cmx cic.cmx deannotate.cmi
cicParser.cmo: deannotate.cmi cicUniv.cmi cic.cmx cicParser.cmi
cicParser.cmx: deannotate.cmx cicUniv.cmx cic.cmx cicParser.cmi
cicUtil.cmo: cicUniv.cmi cic.cmx cicUtil.cmi
let empty_ugraph = empty_bag, UriManager.UriSet.empty, false
let oblivion_ugraph = empty_bag, UriManager.UriSet.empty, true
+(* FG: default choice for a ugraph ??? *)
+let default_ugraph = oblivion_ugraph
let current_index_anon = ref (-1)
let current_index_named = ref (-1)
(* an universe that does nothing: i.e. no constraints are kept, no merges.. *)
val oblivion_ugraph: universe_graph
+(* one of the previous two, no set to empty_ugraph *)
+val default_ugraph: universe_graph
+
+
(*
These are the real functions to add eq/ge/gt constraints
to the passed graph, returning an updated graph or raising
disambiguate.cmi
disambiguate.cmx: disambiguateTypes.cmx disambiguateChoices.cmx \
disambiguate.cmi
-number_notation.cmo: disambiguateChoices.cmi
-number_notation.cmx: disambiguateChoices.cmx
+number_notation.cmo: disambiguateTypes.cmi disambiguateChoices.cmi
+number_notation.cmx: disambiguateTypes.cmx disambiguateChoices.cmx
disambiguate.cmi
disambiguate.cmx: disambiguateTypes.cmx disambiguateChoices.cmx \
disambiguate.cmi
-number_notation.cmo: disambiguateChoices.cmi
-number_notation.cmx: disambiguateChoices.cmx
+number_notation.cmo: disambiguateTypes.cmi disambiguateChoices.cmi
+number_notation.cmx: disambiguateTypes.cmx disambiguateChoices.cmx
freshNamesGenerator.cmi
freshNamesGenerator.cmx: cicTypeChecker.cmx cicSubstitution.cmx \
freshNamesGenerator.cmi
+cicDischarge.cmo: cicEnvironment.cmi cicDischarge.cmi
+cicDischarge.cmx: cicEnvironment.cmx cicDischarge.cmi
freshNamesGenerator.cmi
freshNamesGenerator.cmx: cicTypeChecker.cmx cicSubstitution.cmx \
freshNamesGenerator.cmi
+cicDischarge.cmo: cicEnvironment.cmi cicDischarge.cmi
+cicDischarge.cmx: cicEnvironment.cmx cicDischarge.cmi
cicReduction.mli \
cicTypeChecker.mli \
freshNamesGenerator.mli \
+ cicDischarge.mli \
$(NULL)
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
--- /dev/null
+(* Copyright (C) 2003-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+module UM = UriManager
+module C = Cic
+module Un = CicUniv
+module E = CicEnvironment
+
+let hashtbl_size = 11
+
+let not_implemented =
+ "discharge of current proofs is not implemented yet"
+
+(* helper functions *********************************************************)
+
+let list_pos found l =
+ let rec aux n = function
+ | [] -> raise Not_found
+ | hd :: tl -> if found hd then n else aux (succ n) tl
+ in
+ aux 0 l
+
+let sh a b = if a == b then a else b
+
+let rec list_map_sh map l = match l with
+ | [] -> l
+ | hd :: tl ->
+ let hd', tl' = map hd, list_map_sh map tl in
+ if hd' == hd && tl' == tl then l else
+ sh hd hd' :: sh tl tl'
+
+let flatten = function
+ | C.Appl vs :: tl -> vs @ tl
+ | ts -> ts
+
+let vars_of_uri uri =
+ let obj, _ = E.get_obj Un.default_ugraph uri in
+ match obj with
+ | C.Constant (_, _, _, vars, _)
+ | C.Variable (_, _, _, vars, _)
+ | C.InductiveDefinition (_, vars, _, _)
+ | C.CurrentProof (_, _, _, _, vars, _) -> vars
+
+let mk_arg s u =
+ try List.assq u s
+ with Not_found -> C.Var (u, [])
+
+(* main functions ***********************************************************)
+
+type status = {
+ du: UM.uri -> UM.uri; (* uri discharge map *)
+ c : C.context; (* var context of this object *)
+ ls: (UM.uri, UM.uri list) Hashtbl.t; (* var lists of subobjects *)
+ rl: UM.uri list; (* reverse var list of this object *)
+ h : int (* relocation index *)
+}
+
+let add st k = {st with h = st.h + k}
+
+let discharge st u = st.h + list_pos (UM.eq u) st.rl
+
+let get_args st u =
+ try Hashtbl.find st.ls u
+ with Not_found ->
+ let args = vars_of_uri u in
+ Hashtbl.add st.ls u args; args
+
+let rec discharge_term st t = match t with
+ | C.Implicit _
+ | C.Sort _
+ | C.Rel _ -> t
+ | C.Const (u, s) ->
+ let args = get_args st u in
+ if args = [] then t else
+ let s = List.map (mk_arg s) args in
+ C.Appl (C.Const (st.du u, []) :: discharge_nsubst st s)
+ | C.MutInd (u, m, s) ->
+ let args = get_args st u in
+ if args = [] then t else
+ let s = List.map (mk_arg s) args in
+ C.Appl (C.MutInd (st.du u, m, []) :: discharge_nsubst st s)
+ | C.MutConstruct (u, m, n, s) ->
+ let args = get_args st u in
+ if args = [] then t else
+ let s = List.map (mk_arg s) args in
+ C.Appl (C.MutConstruct (st.du u, m, n, []) :: discharge_nsubst st s)
+ | C.Var (u, s) ->
+ let args = get_args st u in
+ if args = [] then C.Rel (discharge st u) else
+ let s = List.map (mk_arg s) args in
+ C.Appl (C.Rel (discharge st u) :: discharge_nsubst st s)
+ | C.Meta (i, s) ->
+ let s' = list_map_sh (discharge_usubst st) s in
+ if s' == s then t else C.Meta (i, s')
+ | C.Appl vs ->
+ let vs' = list_map_sh (discharge_term st) vs in
+ if vs' == vs then t else C.Appl (flatten vs')
+ | C.Cast (v, w) ->
+ let v', w' = discharge_term st v, discharge_term st w in
+ if v' = v && w' = w then t else
+ C.Cast (sh v v', sh w w')
+ | C.MutCase (u, m, w, v, vs) ->
+ let w', v', vs' =
+ discharge_term st w, discharge_term st v,
+ list_map_sh (discharge_term st) vs
+ in
+ if w' = w && v' = v && vs' == vs then t else
+ C.MutCase (st.du u, m, sh w w', sh v v', sh vs vs')
+ | C.Prod (b, w, v) ->
+ let w', v' = discharge_term st w, discharge_term (add st 1) v in
+ if w' = w && v' = v then t else
+ C.Prod (b, sh w w', sh v v')
+ | C.Lambda (b, w, v) ->
+ let w', v' = discharge_term st w, discharge_term (add st 1) v in
+ if w' = w && v' = v then t else
+ C.Lambda (b, sh w w', sh v v')
+ | C.LetIn (b, y, w, v) ->
+ let y', w', v' =
+ discharge_term st y, discharge_term st w, discharge_term (add st 1) v
+ in
+ if y' = y && w' = w && v' == v then t else
+ C.LetIn (b, sh y y', sh w w', sh v v')
+ | C.CoFix (i, s) ->
+ let no = List.length s in
+ let s' = list_map_sh (discharge_cofun st no) s in
+ if s' == s then t else C.CoFix (i, s')
+ | C.Fix (i, s) ->
+ let no = List.length s in
+ let s' = list_map_sh (discharge_fun st no) s in
+ if s' == s then t else C.Fix (i, s')
+
+and discharge_nsubst st s =
+ List.map (discharge_term st) s
+
+and discharge_usubst st s = match s with
+ | None -> s
+ | Some t ->
+ let t' = discharge_term st t in
+ if t' == t then s else Some t'
+
+and discharge_cofun st no f =
+ let b, w, v = f in
+ let w', v' = discharge_term st w, discharge_term (add st no) v in
+ if w' = w && v' = v then f else
+ b, sh w w', sh v v'
+
+and discharge_fun st no f =
+ let b, i, w, v = f in
+ let w', v' = discharge_term st w, discharge_term (add st no) v in
+ if w' = w && v' = v then f else
+ b, i, sh w w', sh v v'
+
+let close is_type st t =
+ let map t = function
+ | Some (b, C.Def (v, w)) -> C.LetIn (b, v, w, t)
+ | Some (b, C.Decl w) ->
+ if is_type then C.Prod (b, w, t) else C.Lambda (b, w, t)
+ | None -> assert false
+ in
+ List.fold_left map t st.c
+
+let discharge_con st con =
+ let b, v = con in
+ let v' = discharge_term st v in
+ if v' == v && st.rl = [] then con else b, close true st (sh v v')
+
+let discharge_type st ind_type =
+ let b, ind, w, cons = ind_type in
+ let w', cons' = discharge_term st w, list_map_sh (discharge_con st) cons in
+ if w' == w && cons' == cons && st.rl = [] then ind_type else
+ let w'' = close true st (sh w w') in
+ b, ind, w'', sh cons cons'
+
+let rec discharge_object du obj =
+ let ls = Hashtbl.create hashtbl_size in match obj with
+ | C.Variable (b, None, w, vars, attrs) ->
+ let st = init_status du ls vars in
+ let w' = discharge_term st w in
+ if w' = w && vars = [] then obj else
+ let w'' = close true st (sh w w') in
+ C.Variable (b, None, w'', [], attrs)
+ | C.Variable (b, Some v, w, vars, attrs) ->
+ let st = init_status du ls vars in
+ let w', v' = discharge_term st w, discharge_term st v in
+ if w' = w && v' = v && vars = [] then obj else
+ let w'', v'' = close true st (sh w w'), close false st (sh v v') in
+ C.Variable (b, Some v'', w'', [], attrs)
+ | C.Constant (b, None, w, vars, attrs) ->
+ let st = init_status du ls vars in
+ let w' = discharge_term st w in
+ if w' = w && vars = [] then obj else
+ let w'' = close true st (sh w w') in
+ C.Constant (b, None, w'', [], attrs)
+ | C.Constant (b, Some v, w, vars, attrs) ->
+ let st = init_status du ls vars in
+ let w', v' = discharge_term st w, discharge_term st v in
+ if w' = w && v' = v && vars = [] then obj else
+ let w'', v'' = close true st (sh w w'), close false st (sh v v') in
+ C.Constant (b, Some v'', w'', [], attrs)
+ | C.InductiveDefinition (types, vars, lpsno, attrs) ->
+ let st = init_status du ls vars in
+ let types' = list_map_sh (discharge_type st) types in
+ if types' == types && vars = [] then obj else
+ let lpsno' = lpsno + List.length vars in
+ C.InductiveDefinition (sh types types', [], lpsno', attrs)
+ | C.CurrentProof _ ->
+ HLog.warn not_implemented; obj
+
+and discharge_uri du uri =
+ let obj, _ = E.get_obj Un.default_ugraph uri in
+ let obj' = discharge_object du obj in
+ obj', obj' == obj
+
+and discharge_vars du vars =
+ let map u =
+ match discharge_uri du u with
+ | C.Variable (b, None, w, _, _), _ -> Some (C.Name b, C.Decl w)
+ | C.Variable (b, Some v, w, _, _), _ -> Some (C.Name b, C.Def (v, w))
+ | _ -> None
+ in
+ List.rev_map map vars
+
+and init_status du ls vars =
+ let c, rl = discharge_vars du vars, List.rev vars in
+ {du = du; c = c; ls = ls; rl = rl; h = 1}
--- /dev/null
+(* Copyright (C) 2003-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* discharges the explicit variables of the given object (with sharing) *)
+(* the first argument is a map for relocating the uris of the dependencdes *)
+val discharge_object:
+ (UriManager.uri -> UriManager.uri) -> Cic.obj -> Cic.obj
+
+(* applies the previous function to the object at the given uri *)
+(* returns true if the object does not need discharging *)
+val discharge_uri:
+ (UriManager.uri -> UriManager.uri) -> UriManager.uri -> Cic.obj * bool
boxPp.cmi
boxPp.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \
boxPp.cmi
-cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi boxPp.cmi box.cmi \
+cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi box.cmi \
cicNotationPres.cmi
-cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx boxPp.cmx box.cmx \
+cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx box.cmx \
cicNotationPres.cmi
content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
cicNotationPres.cmi box.cmi content2pres.cmi
-cicNotationPres.cmi: mpresentation.cmi box.cmi
+termContentPres.cmi: cicNotationParser.cmi
boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi
+cicNotationPres.cmi: mpresentation.cmi box.cmi
content2pres.cmi: cicNotationPres.cmi
sequent2pres.cmi: cicNotationPres.cmi
renderingAttrs.cmo: renderingAttrs.cmi
content2presMatcher.cmo: content2presMatcher.cmi
content2presMatcher.cmx: content2presMatcher.cmi
termContentPres.cmo: renderingAttrs.cmi content2presMatcher.cmi \
- termContentPres.cmi
+ cicNotationParser.cmi termContentPres.cmi
termContentPres.cmx: renderingAttrs.cmx content2presMatcher.cmx \
- termContentPres.cmi
-cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi box.cmi \
- cicNotationPres.cmi
-cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx box.cmx \
- cicNotationPres.cmi
+ cicNotationParser.cmx termContentPres.cmi
boxPp.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \
boxPp.cmi
boxPp.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \
boxPp.cmi
+cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi box.cmi \
+ cicNotationPres.cmi
+cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx box.cmx \
+ cicNotationPres.cmi
content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
cicNotationPres.cmi box.cmi content2pres.cmi
content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
fourierR.cmi: proofEngineTypes.cmi
fwdSimplTactic.cmi: proofEngineTypes.cmi
statefulProofEngine.cmi: proofEngineTypes.cmi
-tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi
-declarative.cmi: universe.cmi proofEngineTypes.cmi
+tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi
+declarative.cmi: universe.cmi proofEngineTypes.cmi auto.cmi
proofEngineTypes.cmo: proofEngineTypes.cmi
proofEngineTypes.cmx: proofEngineTypes.cmi
proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi
proofEngineStructuralRules.cmx: proofEngineTypes.cmx \
proofEngineStructuralRules.cmi
primitiveTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
- proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi
+ proofEngineStructuralRules.cmi proofEngineReduction.cmi \
+ proofEngineHelpers.cmi primitiveTactics.cmi
primitiveTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
- proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmi
+ proofEngineStructuralRules.cmx proofEngineReduction.cmx \
+ proofEngineHelpers.cmx primitiveTactics.cmi
hashtbl_equiv.cmo: hashtbl_equiv.cmi
hashtbl_equiv.cmx: hashtbl_equiv.cmi
metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
paramodulation/indexing.cmx paramodulation/founif.cmx \
paramodulation/equality.cmx paramodulation/saturation.cmi
-variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
- proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
+variousTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
variousTactics.cmi
-variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \
- proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
+variousTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
variousTactics.cmi
-compose.cmo: variousTactics.cmi proofEngineTypes.cmi primitiveTactics.cmi \
- closeCoercionGraph.cmi compose.cmi
-compose.cmx: variousTactics.cmx proofEngineTypes.cmx primitiveTactics.cmx \
- closeCoercionGraph.cmx compose.cmi
+compose.cmo: proofEngineTypes.cmi primitiveTactics.cmi closeCoercionGraph.cmi \
+ compose.cmi
+compose.cmx: proofEngineTypes.cmx primitiveTactics.cmx closeCoercionGraph.cmx \
+ compose.cmi
introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
introductionTactics.cmi
introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
proofEngineStructuralRules.cmx proofEngineReduction.cmx \
proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \
equalityTactics.cmi
-auto.cmo: paramodulation/utils.cmi universe.cmi paramodulation/subst.cmi \
- paramodulation/saturation.cmi proofEngineTypes.cmi \
- proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
- metadataQuery.cmi paramodulation/indexing.cmi equalityTactics.cmi \
- paramodulation/equality.cmi autoTypes.cmi autoCache.cmi auto.cmi
-auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/subst.cmx \
- paramodulation/saturation.cmx proofEngineTypes.cmx \
- proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
- metadataQuery.cmx paramodulation/indexing.cmx equalityTactics.cmx \
- paramodulation/equality.cmx autoTypes.cmx autoCache.cmx auto.cmi
+auto.cmo: paramodulation/utils.cmi universe.cmi paramodulation/saturation.cmi \
+ proofEngineTypes.cmi proofEngineReduction.cmi proofEngineHelpers.cmi \
+ primitiveTactics.cmi metadataQuery.cmi paramodulation/indexing.cmi \
+ equalityTactics.cmi paramodulation/equality.cmi autoTypes.cmi \
+ autoCache.cmi auto.cmi
+auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/saturation.cmx \
+ proofEngineTypes.cmx proofEngineReduction.cmx proofEngineHelpers.cmx \
+ primitiveTactics.cmx metadataQuery.cmx paramodulation/indexing.cmx \
+ equalityTactics.cmx paramodulation/equality.cmx autoTypes.cmx \
+ autoCache.cmx auto.cmi
destructTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
proofEngineStructuralRules.cmi proofEngineHelpers.cmi \
primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \
fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \
eliminationTactics.cmx destructTactic.cmx compose.cmx \
closeCoercionGraph.cmx auto.cmx tactics.cmi
-declarative.cmo: universe.cmi tactics.cmi tacticals.cmi proofEngineTypes.cmi \
+declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi \
declarative.cmi
-declarative.cmx: universe.cmx tactics.cmx tacticals.cmx proofEngineTypes.cmx \
+declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx auto.cmx \
declarative.cmi
fourierR.cmi: proofEngineTypes.cmi
fwdSimplTactic.cmi: proofEngineTypes.cmi
statefulProofEngine.cmi: proofEngineTypes.cmi
-tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi
-declarative.cmi: universe.cmi proofEngineTypes.cmi
+tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi
+declarative.cmi: universe.cmi proofEngineTypes.cmi auto.cmi
proofEngineTypes.cmo: proofEngineTypes.cmi
proofEngineTypes.cmx: proofEngineTypes.cmi
proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi
proofEngineStructuralRules.cmx: proofEngineTypes.cmx \
proofEngineStructuralRules.cmi
primitiveTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
- proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi
+ proofEngineStructuralRules.cmi proofEngineReduction.cmi \
+ proofEngineHelpers.cmi primitiveTactics.cmi
primitiveTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
- proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmi
+ proofEngineStructuralRules.cmx proofEngineReduction.cmx \
+ proofEngineHelpers.cmx primitiveTactics.cmi
hashtbl_equiv.cmo: hashtbl_equiv.cmi
hashtbl_equiv.cmx: hashtbl_equiv.cmi
metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
paramodulation/indexing.cmx paramodulation/founif.cmx \
paramodulation/equality.cmx paramodulation/saturation.cmi
-variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
- proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
+variousTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
variousTactics.cmi
-variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \
- proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
+variousTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
variousTactics.cmi
-compose.cmo: variousTactics.cmi proofEngineTypes.cmi primitiveTactics.cmi \
- closeCoercionGraph.cmi compose.cmi
-compose.cmx: variousTactics.cmx proofEngineTypes.cmx primitiveTactics.cmx \
- closeCoercionGraph.cmx compose.cmi
+compose.cmo: proofEngineTypes.cmi primitiveTactics.cmi closeCoercionGraph.cmi \
+ compose.cmi
+compose.cmx: proofEngineTypes.cmx primitiveTactics.cmx closeCoercionGraph.cmx \
+ compose.cmi
introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
introductionTactics.cmi
introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
proofEngineStructuralRules.cmx proofEngineReduction.cmx \
proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \
equalityTactics.cmi
-auto.cmo: paramodulation/utils.cmi universe.cmi paramodulation/subst.cmi \
- paramodulation/saturation.cmi proofEngineTypes.cmi \
- proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
- metadataQuery.cmi paramodulation/indexing.cmi equalityTactics.cmi \
- paramodulation/equality.cmi autoTypes.cmi autoCache.cmi auto.cmi
-auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/subst.cmx \
- paramodulation/saturation.cmx proofEngineTypes.cmx \
- proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
- metadataQuery.cmx paramodulation/indexing.cmx equalityTactics.cmx \
- paramodulation/equality.cmx autoTypes.cmx autoCache.cmx auto.cmi
+auto.cmo: paramodulation/utils.cmi universe.cmi paramodulation/saturation.cmi \
+ proofEngineTypes.cmi proofEngineReduction.cmi proofEngineHelpers.cmi \
+ primitiveTactics.cmi metadataQuery.cmi paramodulation/indexing.cmi \
+ equalityTactics.cmi paramodulation/equality.cmi autoTypes.cmi \
+ autoCache.cmi auto.cmi
+auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/saturation.cmx \
+ proofEngineTypes.cmx proofEngineReduction.cmx proofEngineHelpers.cmx \
+ primitiveTactics.cmx metadataQuery.cmx paramodulation/indexing.cmx \
+ equalityTactics.cmx paramodulation/equality.cmx autoTypes.cmx \
+ autoCache.cmx auto.cmi
destructTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
proofEngineStructuralRules.cmi proofEngineHelpers.cmi \
primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \
fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \
eliminationTactics.cmx destructTactic.cmx compose.cmx \
closeCoercionGraph.cmx auto.cmx tactics.cmi
-declarative.cmo: universe.cmi tactics.cmi tacticals.cmi proofEngineTypes.cmi \
+declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi \
declarative.cmi
-declarative.cmx: universe.cmx tactics.cmx tacticals.cmx proofEngineTypes.cmx \
+declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx auto.cmx \
declarative.cmi
projects / helm.git / commitdiff