X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Facic2Procedural.ml;h=c9423268ccb9d144cb1c536ee5cd258307d780b4;hb=0baaadae4614d4948d659c86aa3fa2c6172bc397;hp=7fd8290ba224783c9856a4cb84a1e2576749c90e;hpb=c465c17581bf606e0330cbd89b238279c184ad35;p=helm.git diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 7fd8290ba..c9423268c 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -26,6 +26,7 @@ module C = Cic module I = CicInspect module D = Deannotate +module S = CicSubstitution module TC = CicTypeChecker module Un = CicUniv module UM = UriManager @@ -34,9 +35,9 @@ module HObj = HelmLibraryObjects module A = Cic2acic module Ut = CicUtil module E = CicEnvironment -module PEH = ProofEngineHelpers -module PER = ProofEngineReduction module Pp = CicPp +module PEH = ProofEngineHelpers +module HEL = HExtlib module Cl = ProceduralClassify module T = ProceduralTypes @@ -59,8 +60,8 @@ let cic = D.deannotate_term let split2_last l1 l2 = try let n = pred (List.length l1) in - let before1, after1 = T.list_split n l1 in - let before2, after2 = T.list_split n l2 in + let before1, after1 = HEL.split_nth n l1 in + let before2, after2 = HEL.split_nth n l2 in before1, before2, List.hd after1, List.hd after2 with Invalid_argument _ -> failwith "A2P.split2_last" @@ -155,20 +156,50 @@ try ty with e -> failwith (msg ^ ": " ^ Printexc.to_string e) +let get_entry st id = + let rec aux = function + | [] -> assert false + | Some (C.Name name, e) :: _ when name = id -> e + | _ :: tl -> aux tl + in + aux st.context + (* proof construction *******************************************************) let unused_premise = "UNUSED" +let mk_exp_args hd tl classes synth = + let meta id = C.AImplicit (id, None) in + let map v (cl, b) = + if I.overlaps synth cl && b then v else meta "" + in + let rec aux = function + | [] -> [] + | hd :: tl -> if hd = meta "" then aux tl else List.rev (hd :: tl) + in + let args = T.list_rev_map2 map tl classes in + let args = aux args in + if args = [] then hd else C.AAppl ("", hd :: args) + let convert st ?name v = match get_inner_types st v with - | None -> [] - | Some (st, et) -> - let cst, cet = cic st, cic et in - if PER.alpha_equivalence cst cet then [] else + | None -> [] + | Some (sty, ety) -> let e = Cn.mk_pattern 0 (T.mk_arel 1 "") in + let csty, cety = cic sty, cic ety in + if Ut.alpha_equivalence csty cety then [] else match name with - | None -> [T.Change (st, et, None, e, "")] - | Some id -> [T.Change (st, et, Some (id, id), e, ""); T.ClearBody (id, "")] + | None -> [T.Change (sty, ety, None, e, "")] + | Some (id, i) -> + begin match get_entry st id with + | C.Def _ -> [T.ClearBody (id, "")] + | C.Decl w -> + let w = S.lift i w in + if Ut.alpha_equivalence csty w then [] + else + [T.Note (Pp.ppterm csty); T.Note (Pp.ppterm w); + T.Change (sty, ety, Some (id, id), e, "")] + end let get_intro = function | C.Anonymous -> unused_premise @@ -180,7 +211,7 @@ let mk_intros st script = T.Intros (Some count, List.rev st.intros, "") :: script let mk_arg st = function - | C.ARel (_, _, _, name) as what -> convert st ~name what + | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what | _ -> [] let mk_fwd_rewrite st dtext name tl direction = @@ -217,10 +248,10 @@ and proc_letin st what name v t = | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl -> mk_fwd_rewrite st dtext intro tl false | v -> - let qs = [[T.Id ""]; proc_proof (next st) v] in + let qs = [proc_proof (next st) v; [T.Id ""]] in [T.Branch (qs, ""); T.Cut (intro, ity, dtext)] in - C.Decl (get_type "TC1" st v), rqv + C.Decl (cic ity), rqv | None -> C.Def (cic v, None), [T.LetIn (intro, v, dtext)] in @@ -248,11 +279,19 @@ and proc_appl st what hd tl = let script = if proceed then let ty = get_type "TC2" st hd in let (classes, rc) as h = Cl.classify st.context ty in + let goal_arity = match get_inner_types st what with + | None -> 0 + | Some (ity, _) -> snd (PEH.split_with_whd (st.context, cic ity)) + in let argsno = List.length classes in - let diff = argsno - List.length tl in - if diff <> 0 then failwith (Printf.sprintf "NOT TOTAL: %i %s |--- %s" diff (Pp.ppcontext st.context) (Pp.ppterm (cic hd))); - let synth = I.S.singleton 0 in - let text = Printf.sprintf "%u %s" argsno (Cl.to_string h) in + let decurry = argsno - List.length tl in + let diff = goal_arity - decurry in + if diff < 0 then failwith (Printf.sprintf "NOT TOTAL: %i %s |--- %s" diff (Pp.ppcontext st.context) (Pp.ppterm (cic hd))); + let rec mk_synth a n = + if n < 0 then a else mk_synth (I.S.add n a) (pred n) + in + let synth = mk_synth I.S.empty decurry in + let text = "" (* Printf.sprintf "%u %s" argsno (Cl.to_string h) *) in let script = List.rev (mk_arg st hd) @ convert st what in match rc with | Some (i, j) -> @@ -272,6 +311,7 @@ and proc_appl st what hd tl = [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")] | None -> let qs = proc_bkd_proofs (next st) synth classes tl in + let hd = mk_exp_args hd tl classes synth in script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] else [T.Apply (what, dtext)] @@ -283,7 +323,6 @@ and proc_other st what = let script = [T.Note text] in mk_intros st script - and proc_proof st = function | C.ALambda (_, name, w, t) -> proc_lambda st name w t | C.ALetIn (_, name, v, t) as what -> proc_letin st what name v t @@ -299,9 +338,9 @@ try if I.overlaps synth inv then None else if I.S.is_empty inv then Some (proc_proof st v) else Some [T.Apply (v, dtext ^ "dependent")] - in - T.list_map2_filter aux classes ts -with Invalid_argument _ -> failwith "A2P.proc_bkd_proofs" + in + List.rev (T.list_map2_filter aux classes ts) +with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s) (* object costruction *******************************************************)