X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=51b86fa5e092db484f01737a5113db82087f8adc;hb=9af0ac16488f57149c7d02aa5bbee47a81c7c342;hp=95e396003085b59ce219c082beac5d05274258bf;hpb=686ad41d7c9431094c12dae0fa6b84a898c38e84;p=helm.git diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 95e396003..51b86fa5e 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -80,22 +80,16 @@ let tactic_of_ast status ast = | GrafiteAst.Cut (_, ident, term) -> let names = match ident with None -> [] | Some id -> [id] in Tactics.cut ~mk_fresh_name_callback:(namer_of names) term - | GrafiteAst.Decompose (_, types, what, names) -> - let to_type = function - | GrafiteAst.Type (uri, typeno) -> uri, Some typeno - | GrafiteAst.Ident _ -> assert false - in - let user_types = List.rev_map to_type types in - let dbd = LibraryDb.instance () in + | GrafiteAst.Decompose (_, names) -> let mk_fresh_name_callback = namer_of names in - Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what + Tactics.decompose ~mk_fresh_name_callback () | GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe | GrafiteAst.Destruct (_,term) -> Tactics.destruct term - | GrafiteAst.Elim (_, what, using, depth, names) -> + | GrafiteAst.Elim (_, what, using, pattern, depth, names) -> Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) - what + ~pattern what | GrafiteAst.ElimType (_, what, using, depth, names) -> Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) what @@ -151,7 +145,6 @@ let tactic_of_ast status ast = | `Unfold what -> Tactics.unfold ~pattern what | `Whd -> Tactics.whd ~pattern) | GrafiteAst.Reflexivity _ -> Tactics.reflexivity - | GrafiteAst.Rename (_, froms, tos) -> Tactics.rename ~froms ~tos | GrafiteAst.Replace (_, pattern, with_what) -> Tactics.replace ~pattern ~with_what | GrafiteAst.Rewrite (_, direction, t, pattern, names) -> @@ -180,7 +173,8 @@ let tactic_of_ast status ast = | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction t id | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t | GrafiteAst.ExistsElim (_, t, id1, t1, id2, t2) -> - Declarative.existselim t id1 t1 id2 t2 + Declarative.existselim ~dbd:(LibraryDb.instance()) + ~universe:status.GrafiteTypes.universe t id1 t1 id2 t2 | GrafiteAst.Case (_,id,params) -> Declarative.case id params | GrafiteAst.AndElim(_,t,id1,t1,id2,t2) -> Declarative.andelim t id1 t1 id2 t2 | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) -> @@ -331,7 +325,7 @@ prerr_endline("opened: " ^ String.concat ", " (List.map string_of_int opened)); prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int closed_goals)); *) let proof, opened_goals = if needs_reordering then begin - let uri, metasenv_after_tactic, t, ty = proof in + let uri, metasenv_after_tactic, t, ty, attrs = proof in (* prerr_endline ("goal prima del riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof))); *) let reordered_metasenv, opened_goals = reorder_metasenv @@ -339,7 +333,7 @@ prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int clos metasenv_after_refinement metasenv_after_tactic opened goal always_opens_a_goal in - let proof' = uri, reordered_metasenv, t, ty in + let proof' = uri, reordered_metasenv, t, ty, attrs in (* prerr_endline ("goal dopo il riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof'))); *) proof', opened_goals end @@ -684,16 +678,16 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status *) status,[] | GrafiteAst.Print (_,"proofterm") -> - let _,_,p,_ = GrafiteTypes.get_current_proof status in + let _,_,p,_, _ = GrafiteTypes.get_current_proof status in print_endline (AutoTactic.pp_proofterm p); status,[] | GrafiteAst.Print (_,_) -> status,[] | GrafiteAst.Qed loc -> - let uri, metasenv, bo, ty = + let uri, metasenv, bo, ty, attrs = match status.GrafiteTypes.proof_status with - | GrafiteTypes.Proof (Some uri, metasenv, body, ty) -> - uri, metasenv, body, ty - | GrafiteTypes.Proof (None, metasenv, body, ty) -> + | GrafiteTypes.Proof (Some uri, metasenv, body, ty, attrs) -> + uri, metasenv, body, ty, attrs + | GrafiteTypes.Proof (None, metasenv, body, ty, attrs) -> raise (GrafiteTypes.Command_error ("Someone allows to start a theorem without giving the "^ "name/uri. This should be fixed!")) @@ -706,7 +700,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status (GrafiteTypes.Command_error "Proof not completed! metasenv is not empty!"); let name = UriManager.name_of_uri uri in - let obj = Cic.Constant (name,Some bo,ty,[],[]) in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) in let status, lemmas = add_obj uri obj status in {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, @@ -758,7 +752,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let obj = CicRefine.pack_coercion_obj obj in let metasenv = GrafiteTypes.get_proof_metasenv status in match obj with - | Cic.CurrentProof (_,metasenv',bo,ty,_,_) -> + | Cic.CurrentProof (_,metasenv',bo,ty,_, attrs) -> let name = UriManager.name_of_uri uri in if not(CicPp.check name ty) then HLog.error ("Bad name: " ^ name); @@ -790,7 +784,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status ("Theorem already proved: " ^ UriManager.string_of_uri x ^ "\nPlease use a variant.")); end; - let initial_proof = (Some uri, metasenv', bo, ty) in + let initial_proof = (Some uri, metasenv', bo, ty, attrs) in let initial_stack = Continuationals.Stack.of_metasenv metasenv' in { status with GrafiteTypes.proof_status = GrafiteTypes.Incomplete_proof