From 987627a48b2a3c2345d1af2c2a6b1ab78aa90b58 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 28 Nov 2008 18:28:58 +0000 Subject: [PATCH] ng_disambiguation ng_kernel ng_refiner disambiguation: svn:ignore fixed hExtlib: the map of list_findopt takes the position in the list (starts at 0) cicRefine, acic2astMatcher, grafiteEngine: updated accordingly cicUtil cicDischarge: bug fixes cicSubstitution: new function lift_map for non-linear relocation proceduralOptimizer: initial support for contrlling critical optimizations --- .../acic_content/acic2astMatcher.ml | 2 +- .../acic_procedural/proceduralOptimizer.ml | 15 +- helm/software/components/cic/cicUtil.ml | 40 +++-- .../cic_proof_checking/cicDischarge.ml | 140 ++++++++++++++---- .../cic_proof_checking/cicSubstitution.ml | 7 +- .../cic_proof_checking/cicSubstitution.mli | 7 +- .../components/cic_unification/cicRefine.ml | 4 +- helm/software/components/extlib/hExtlib.ml | 8 +- helm/software/components/extlib/hExtlib.mli | 2 +- .../grafite_engine/grafiteEngine.ml | 2 +- 10 files changed, 169 insertions(+), 58 deletions(-) diff --git a/helm/software/components/acic_content/acic2astMatcher.ml b/helm/software/components/acic_content/acic2astMatcher.ml index c71108320..908aa942f 100644 --- a/helm/software/components/acic_content/acic2astMatcher.ml +++ b/helm/software/components/acic_content/acic2astMatcher.ml @@ -79,7 +79,7 @@ struct let compiler rows = let match_cb rows matched_terms constructors = HExtlib.list_findopt - (fun (pl,pid) -> + (fun (pl,pid) _ -> let env = try List.map2 diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index 1b4cbd8e0..f1840cf7c 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -46,6 +46,8 @@ let debug = ref false (* term optimization ********************************************************) +let critical = ref true + type status = { dummy: unit; info: string @@ -68,8 +70,8 @@ let clear_absts m = aux 0 (pred n) (S.lift (-1) t) | t when n > 0 -> Printf.eprintf "PO.clear_absts: %u %s\n" n (Pp.ppterm t); - assert false - | t -> t + assert false + | t -> t in aux m @@ -177,7 +179,7 @@ and opt_appl g st es c t vs = in if es then H.list_fold_right_cps g map vs (st, []) else g (st, vs) -and opt_mutcase g st es c uri tyno outty arg cases = +and opt_mutcase_critical g st es c uri tyno outty arg cases = let eliminator = H.get_default_eliminator c uri tyno outty in let lpsno, (_, _, _, constructors) = H.get_ind_type uri tyno in let ps, sort_disp = H.get_ind_parameters c arg in @@ -206,6 +208,13 @@ and opt_mutcase g st es c uri tyno outty arg cases = let x = H.refine c (C.Appl args) in opt_proof g (info st "Optimizer: remove 3") es c x +and opt_mutcase_plain g st es c uri tyno outty arg cases = + let g st v ts = g st (C.MutCase (uri, tyno, outty, v, ts)) in + g st arg cases + +and opt_mutcase g = + if !critical then opt_mutcase_critical g else opt_mutcase_plain g + and opt_cast g st es c t w = let g st t = g (info st "Optimizer: remove 4") t in if es then opt_proof g st es c t else g st t diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml index 484814409..c5061c62f 100644 --- a/helm/software/components/cic/cicUtil.ml +++ b/helm/software/components/cic/cicUtil.ml @@ -628,7 +628,7 @@ 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)) + with Failure "nth" -> out (Printf.sprintf "%u[%i]" i (List.length c - i)) let pp_implict out = function | None -> out "?" @@ -696,7 +696,10 @@ 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 -and pp_attrs out attrs = +let pp_int out i = + out (Printf.sprintf "%u" i) + +let pp_attrs out attrs = let map = function | _ -> () in @@ -705,19 +708,32 @@ and pp_attrs out attrs = let pp_pars out pars = xiter out " (" ", " ")\n" (pp_uri out) pars +let pp_point out point = + if point then out "ind " else out "coind " + +let pp_constructor out (s, w) = + out s; out " of "; pp_term out [] [] w + +let pp_definition out (s, point, w, ts) = + out "let "; pp_point out point; out s; out " of "; pp_term out [] [] w; + xiter out "\ndef " "\nor " "" (pp_constructor out) ts + let pp_obj out = function - | C.Constant (s, None, u, pars, attrs) -> + | C.Constant (s, None, u, pars, attrs) -> out "fun "; pp_attrs out attrs; out s; pp_pars out pars; out " of "; pp_term out [] [] u - | C.Constant (s, Some t, u, pars, attrs) -> + | C.Constant (s, Some t, u, pars, attrs) -> out "let "; pp_attrs out attrs; out s; pp_pars out pars; out " def "; pp_term out [] [] t; out " of "; pp_term out [] [] u - | C.Variable (s, None, u, pars, attrs) -> - out "Local declaration" - | C.Variable (s, Some t, u, pars, attrs) -> - out "Local definition" - | C.CurrentProof (s, e, t, u, pars, attrs) -> + | C.Variable (s, None, u, pars, attrs) -> + out "local fun "; pp_attrs out attrs; out s; pp_pars out pars; + out " of "; pp_term out [] [] u + | C.Variable (s, Some t, u, pars, attrs) -> + out "local let "; pp_attrs out attrs; out s; pp_pars out pars; + out " def "; pp_term out [] [] t; out " of "; pp_term out [] [] u + | C.InductiveDefinition (us, pars, lpsno, attrs) -> + out "Inductive "; pp_attrs out attrs; pp_int out lpsno; pp_pars out pars; + xiter out "" "\n" "" (pp_definition out) us + | C.CurrentProof (s, e, t, u, pars, attrs) -> out "Current Proof" - | C.InductiveDefinition (us, pars, lpno, attrs) -> - out "Inductive Definition" - + diff --git a/helm/software/components/cic_proof_checking/cicDischarge.ml b/helm/software/components/cic_proof_checking/cicDischarge.ml index 066eb72c9..4ad41eef7 100644 --- a/helm/software/components/cic_proof_checking/cicDischarge.ml +++ b/helm/software/components/cic_proof_checking/cicDischarge.ml @@ -29,6 +29,8 @@ module Un = CicUniv module E = CicEnvironment module Ut = CicUtil module TC = CicTypeChecker +module S = CicSubstitution +module X = HExtlib let hashtbl_size = 11 @@ -41,10 +43,23 @@ let out = prerr_string (* helper functions *********************************************************) -let typecheck t = +let rec count_prods n = function + | C.Prod (_, _, t) -> count_prods (succ n) t + | _ -> n + +let get_ind_type_psnos uri tyno = + match E.get_obj Un.default_ugraph uri with + | C.InductiveDefinition (tys, _, lpsno, _), _ -> + let _, _, ty, _ = List.nth tys tyno in + lpsno, count_prods 0 ty + | _ -> assert false + +let typecheck b t = if !debug then begin + out (Printf.sprintf "Pre Check ; %s\n" b); + Ut.pp_term out [] [] t; out "\n"; let _ = TC.type_of_aux' [] [] t Un.default_ugraph in - out "Typecheck : OK\n" + out (Printf.sprintf "Typecheck : %s OK\n" b) end let list_pos found l = @@ -84,13 +99,13 @@ let mk_arg s u = type status = { dn: string -> string; (* name discharge map *) 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 *) + h : int; (* relocation index *) + c : C.context (* local context of this object *) } -let add st k = {st with h = st.h + k} +let add st k es = {st with h = st.h + k; c = List.rev_append es st.c} let discharge st u = st.h + list_pos (UM.eq u) st.rl @@ -100,6 +115,45 @@ let get_args st u = let args = vars_of_uri u in Hashtbl.add st.ls u args; args +let proj_fix (s, _, w, _) = s, w + +let proj_cofix (s, w, _) = s, w + +let mk_context proj discharge_term s = + let map e = + let s, w = proj e in + let w' = discharge_term w in + Some (C.Name s, C.Decl w') + in + List.length s, List.rev_map map s + +let rec split_absts named no c = function + | C.Lambda (s, w, t) -> + let e = Some (s, C.Decl w) in + let named = named && s <> C.Anonymous in + split_absts named (succ no) (e :: c) t + | t -> + named, no, c, t + +let close is_type c 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 c + +let relocate to_what from_what k m = + try + let u = List.nth from_what (m - k) in + let map v m = if UM.eq u v then Some m else None in + match X.list_findopt map to_what with + | Some m -> m + k + | None -> raise (Failure "nth") + with + | Failure "nth" -> assert false + let rec discharge_term st t = match t with | C.Implicit _ | C.Sort _ @@ -141,29 +195,60 @@ let rec discharge_term st t = match t with discharge_term st w, discharge_term st v, list_map_sh (discharge_term st) vs in +(* BEGIN FIX OUT TYPE *) + let lpsno, psno = get_ind_type_psnos u m in + let rpsno = psno - lpsno in + let named, frpsno, wc, wb = split_absts true 0 [] w' in + let w' = +(* No fixing needed *) + if frpsno = succ rpsno then w' else +(* Fixing needed, no right parametes *) + if frpsno = rpsno && rpsno = 0 then + let vty, _ = TC.type_of_aux' [] st.c v' Un.default_ugraph in + if !debug then begin + out "VTY: "; Ut.pp_term out [] st.c vty; out "\n" + end; + C.Lambda (C.Anonymous, vty, S.lift 1 wb) + else +(* Fixing needed, some right parametes *) + if frpsno = rpsno then + let vty, _ = TC.type_of_aux' [] st.c v' Un.default_ugraph in + if !debug then begin + out "VTY: "; Ut.pp_term out [] st.c vty; out "\n" + end; + let vty, wb = S.lift rpsno vty, S.lift (succ rpsno) wb in + close false wc (C.Lambda (C.Anonymous, vty, wb)) +(* This case should not happen *) + else assert false + in +(* END FIX OUT TYPE *) if UM.eq u u' && w' == w && v' == v && vs' == vs then t else C.MutCase (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 + let w' = discharge_term st w in + let es = [Some (b, C.Decl w')] in + let v' = discharge_term (add st 1 es) 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 + let w' = discharge_term st w in + let es = [Some (b, C.Decl w')] in + let v' = discharge_term (add st 1 es) 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 + let y', w' = discharge_term st y, discharge_term st w in + let es = [Some (b, C.Def (y, w'))] in + let v' = discharge_term (add st 1 es) 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 + let no, es = mk_context proj_cofix (discharge_term st) s in + let s' = list_map_sh (discharge_cofun st no es) 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 + let no, es = mk_context proj_fix (discharge_term st) s in + let s' = list_map_sh (discharge_fun st no es) s in if s' == s then t else C.Fix (i, s') and discharge_nsubst st s = @@ -175,26 +260,19 @@ and discharge_usubst st s = match s with let t' = discharge_term st t in if t' == t then s else Some t' -and discharge_cofun st no f = +and discharge_cofun st no es f = let b, w, v = f in - let w', v' = discharge_term st w, discharge_term (add st no) v in + let w', v' = discharge_term st w, discharge_term (add st no es) v in if w' == w && v' == v then f else b, sh w w', sh v v' -and discharge_fun st no f = +and discharge_fun st no es f = let b, i, w, v = f in - let w', v' = discharge_term st w, discharge_term (add st no) v in + let w', v' = discharge_term st w, discharge_term (add st no es) 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 close is_type st = close is_type st.c let discharge_con st con = let b, v = con in @@ -215,28 +293,28 @@ let rec discharge_object dn du obj = let w' = discharge_term st w in if w' == w && vars = [] then obj else let w'' = sh w w' in - let _ = typecheck w'' in +(* We do not typecheck because variables are not closed *) C.Variable (dn b, None, w'', [], attrs) | C.Variable (b, Some v, w, vars, attrs) -> let st = init_status dn 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'' = sh w w', sh v v' in - let _ = typecheck (C.Cast (v'', w'')) in +(* We do not typecheck because variables are not closed *) C.Variable (dn b, Some v'', w'', [], attrs) | C.Constant (b, None, w, vars, attrs) -> let st = init_status dn 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 - let _ = typecheck w'' in + let _ = typecheck (dn b) w'' in C.Constant (dn b, None, w'', [], attrs) | C.Constant (b, Some v, w, vars, attrs) -> let st = init_status dn 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 - let _ = typecheck (C.Cast (v'', w'')) in + let _ = typecheck (dn b) (C.Cast (v'', w'')) in C.Constant (dn b, Some v'', w'', [], attrs) | C.InductiveDefinition (types, vars, lpsno, attrs) -> let st = init_status dn du ls vars in @@ -271,4 +349,4 @@ and discharge_vars dn du vars = and init_status dn du ls vars = let c, rl = discharge_vars dn du vars, List.rev vars in - {dn = dn; du = du; c = c; ls = ls; rl = rl; h = 1} + {dn = dn; du = du; ls = ls; rl = rl; h = 1; c = c} diff --git a/helm/software/components/cic_proof_checking/cicSubstitution.ml b/helm/software/components/cic_proof_checking/cicSubstitution.ml index ba2c8f723..d111b15b5 100644 --- a/helm/software/components/cic_proof_checking/cicSubstitution.ml +++ b/helm/software/components/cic_proof_checking/cicSubstitution.ml @@ -40,7 +40,7 @@ let debug_print = fun _ -> () ;; -let lift_from k n = +let lift_map k map = let rec liftaux k = let module C = Cic in function @@ -48,7 +48,7 @@ let lift_from k n = if m < k then C.Rel m else - C.Rel (m + n) + C.Rel (map k m) | C.Var (uri,exp_named_subst) -> let exp_named_subst' = List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst @@ -108,6 +108,9 @@ let lift_from k n = in liftaux k +let lift_from k n = + lift_map k (fun _ m -> m + n) + let lift n t = if n = 0 then t diff --git a/helm/software/components/cic_proof_checking/cicSubstitution.mli b/helm/software/components/cic_proof_checking/cicSubstitution.mli index 36291fb18..68311c68c 100644 --- a/helm/software/components/cic_proof_checking/cicSubstitution.mli +++ b/helm/software/components/cic_proof_checking/cicSubstitution.mli @@ -35,11 +35,16 @@ exception ReferenceToInductiveDefinition;; (* since it needs to restrict the metavariables in case of failure *) val lift : int -> Cic.term -> Cic.term - (* lift from n t *) (* as lift but lifts only indexes >= from *) val lift_from: int -> int -> Cic.term -> Cic.term +(* lift map t *) +(* as lift_from but lifts indexes by applying a map to them + the first argument of the map is the current depth *) +(* FG: this is used in CicDischarge to perform non-linear relocation *) +val lift_map: int -> (int -> int -> int) -> Cic.term -> Cic.term + (* subst t1 t2 *) (* substitutes [t1] for [Rel 1] in [t2] *) (* if avoid_beta_redexes is true (default: false) no new beta redexes *) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index a263a2eb4..0168d2d75 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1191,7 +1191,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci | CoercGraph.SomeCoercion candidates -> let selected = HExtlib.list_findopt - (function (metasenv,last,c) -> + (fun (metasenv,last,c) _ -> match c with | c when not (CoercGraph.is_composite c) -> debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c)); @@ -1345,7 +1345,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci ugraph in match HExtlib.list_findopt - (fun (he,hetype,subst,metasenv,ugraph) -> + (fun (he,hetype,subst,metasenv,ugraph) _ -> (* {{{ *)debug_print (lazy ("Try fix: "^ CicMetaSubst.ppterm_in_context ~metasenv subst he context)); debug_print (lazy (" of type: "^ diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index 3fe5c0a7d..523913cbf 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -239,14 +239,14 @@ let list_concat ?(sep = []) = aux [] let rec list_findopt f l = - let rec aux = function + let rec aux k = function | [] -> None | x::tl -> - (match f x with - | None -> aux tl + (match f x k with + | None -> aux (succ k) tl | Some _ as rc -> rc) in - aux l + aux 0 l let split_nth n l = let rec aux acc n l = diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli index dae914477..d8c4eccd0 100644 --- a/helm/software/components/extlib/hExtlib.mli +++ b/helm/software/components/extlib/hExtlib.mli @@ -87,7 +87,7 @@ val filter_map: ('a -> 'b option) -> 'a list -> 'b list (** filter + map *) val list_rev_map_filter: ('a -> 'b option) -> 'a list -> 'b list val list_rev_map_filter_fold: ('c -> 'a -> 'c * 'b option) -> 'c -> 'a list -> 'c * 'b list val list_concat: ?sep:'a list -> 'a list list -> 'a list (**String.concat-like*) -val list_findopt: ('a -> 'b option) -> 'a list -> 'b option +val list_findopt: ('a -> int -> 'b option) -> 'a list -> 'b option val flatten_map: ('a -> 'b list) -> 'a list -> 'b list val list_last: 'a list -> 'a val list_mapi: ('a -> int -> 'b) -> 'a list -> 'b list diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index d9c460849..f58f4303c 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -560,7 +560,7 @@ let eval_comment status c = status * information inside the moo *) let add_coercions_of_record_to_moo obj lemmas status = let attributes = CicUtil.attributes_of_obj obj in - let is_record = function `Class (`Record att) -> Some att | _-> None in + let is_record x _ = match x with `Class (`Record att) -> Some att | _-> None in match HExtlib.list_findopt is_record attributes with | None -> status,[] | Some fields -> -- 2.39.2