X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2Fprocedural2.ml;h=7ac82a0a63989326d736864adab9ca2e866d372f;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=958fc4abbd0f80b5db55d89c48872193859260b0;hpb=d3548c16f481b14ce94e64c790bc767c59590050;p=helm.git diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml index 958fc4abb..7ac82a0a6 100644 --- a/helm/software/components/acic_procedural/procedural2.ml +++ b/helm/software/components/acic_procedural/procedural2.ml @@ -64,8 +64,8 @@ let debug = ref false let split2_last l1 l2 = try let n = pred (List.length l1) in - let before1, after1 = HEL.split_nth n l1 in - let before2, after2 = HEL.split_nth n l2 in + let before1, after1 = HEL.split_nth "P2 1" n l1 in + let before2, after2 = HEL.split_nth "P2 2" n l2 in before1, before2, List.hd after1, List.hd after2 with Invalid_argument _ -> failwith "A2P.split2_last" @@ -140,15 +140,6 @@ try with Not_found -> None with Invalid_argument _ -> failwith "A2P.get_inner_types" -let is_proof st v = -try - let id = Ut.id_of_annterm v in - try match Hashtbl.find st.sorts id with - | `Prop -> true - | _ -> false - with Not_found -> H.is_proof st.context (H.cic v) -with Invalid_argument _ -> failwith "P1.is_proof" - let get_entry st id = let rec aux = function | [] -> assert false @@ -195,28 +186,30 @@ let mk_exp_args hd tl classes synth = if args = [] then b, hd else b, C.AAppl ("", hd :: args) let mk_convert st ?name sty ety note = + let ppterm t = + let a = ref "" in Ut.pp_term (fun s -> a := !a ^ s) [] st.context t; !a + in let e = Cn.hole "" in let csty, cety = H.cic sty, H.cic ety in - let script = + let note = if !debug then let sname = match name with None -> "" | Some (id, _) -> id in - let note = Printf.sprintf "%s: %s\nSINTH: %s\nEXP: %s" - note sname (Pp.ppterm csty) (Pp.ppterm cety) - in - [T.Note note] - else [] + Printf.sprintf "%s: %s\nSINTH: %s\nEXP: %s" + note sname (ppterm csty) (ppterm cety) + else "" in - assert (Ut.is_sober st.context csty); - assert (Ut.is_sober st.context cety); - if Ut.alpha_equivalence csty cety then script else + if H.alpha_equivalence ~flatten:true st.context csty cety then [T.Note note] else let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in match name with - | None -> T.Change (sty, ety, None, e, "") :: script + | None -> [T.Change (sty, ety, None, e, note)] | Some (id, i) -> begin match get_entry st id with - | C.Def _ -> assert false (* T.ClearBody (id, "") :: script *) + | C.Def _ -> + [T.Change (ety, sty, Some (id, Some id), e, note); + T.ClearBody (id, "") + ] | C.Decl _ -> - T.Change (ety, sty, Some (id, Some id), e, "") :: script + [T.Change (ety, sty, Some (id, Some id), e, note)] end let convert st ?name v = @@ -288,8 +281,10 @@ and proc_letin st what name v w t = let intro = get_intro name in let proceed, dtext = test_depth st in let script = if proceed then - let st, hyp, rqv = match get_inner_types st v with - | Some (ity, _) -> + let st, hyp, rqv = match get_inner_types st what, get_inner_types st v with + | Some (C.ALetIn _, _), _ -> + st, C.Def (H.cic v, H.cic w), [T.Intros (Some 1, [intro], dtext)] + | _, Some (ity, _) -> let st, rqv = match v with | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right st hd tl -> mk_fwd_rewrite st dtext intro tl true v t ity @@ -302,7 +297,7 @@ and proc_letin st what name v w t = st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)] in st, C.Decl (H.cic ity), rqv - | None -> + | _, None -> st, C.Def (H.cic v, H.cic w), [T.LetIn (intro, v, dtext)] in let entry = Some (name, hyp) in @@ -393,7 +388,7 @@ and proc_case st what uri tyno u v ts = let qs = proc_bkd_proofs (next st) synth names classes ts in let lpsno, _ = H.get_ind_type uri tyno in let ps, _ = H.get_ind_parameters st.context (H.cic v) in - let _, rps = HEL.split_nth lpsno ps in + let _, rps = HEL.split_nth "P2 3" lpsno ps in let rpsno = List.length rps in let e = Cn.mk_pattern rpsno u in let text = "" in @@ -458,48 +453,7 @@ try with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s) -(* object costruction *******************************************************) - -let th_flavours = [`Theorem; `Lemma; `Remark; `Fact] - -let def_flavours = [`Definition; `Variant] - -let get_flavour st v attrs = - let rec aux = function - | [] -> - if is_proof st v then List.hd th_flavours else List.hd def_flavours - | `Flavour fl :: _ -> fl - | _ :: tl -> aux tl - in - let flavour_map x y = match x, y with - | None, G.IPAs flavour -> Some flavour - | _ -> x - in - match List.fold_left flavour_map None st.params with - | Some fl -> fl - | None -> aux attrs - -let proc_obj ?(info="") st = function - | C.AConstant (_, _, s, Some v, t, [], attrs) -> - begin match get_flavour st v attrs with - | flavour when List.mem flavour th_flavours -> - let ast = proc_proof st v in - let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in - let text = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s" - "COMMENTS" info "Tactics" steps "Final nodes" nodes "END" - in - T.Statement (flavour, Some s, t, None, "") :: ast @ [T.Qed text] - | flavour when List.mem flavour def_flavours -> - [T.Statement (flavour, Some s, t, Some v, "")] - | _ -> - failwith "not a theorem, definition, axiom or inductive type" - end - | C.AConstant (_, _, s, None, t, [], attrs) -> - [T.Statement (`Axiom, Some s, t, None, "")] - | C.AInductiveDefinition (_, types, [], lpsno, attrs) -> - [T.Inductive (types, lpsno, "")] - | _ -> - failwith "not a theorem, definition, axiom or inductive type" +(* initialization ***********************************************************) let init ~ids_to_inner_sorts ~ids_to_inner_types params context = let depth_map x y = match x, y with