X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=bc56ce35dd7b16678b4553a63353c13c24866b97;hb=13553fb82419f58ab61131bd4a6e04352e388b50;hp=0d2fb682ed78b98ec293f6e26b6ce94353a7c1e2;hpb=2c80e9d9409119febcab9c08d6e6cad702384169;p=helm.git diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 0d2fb682e..bc56ce35d 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -33,15 +33,30 @@ exception IncludedFileNotCompiled of string * string exception Macro of GrafiteAst.loc * (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -exception ReadOnlyUri of string type 'a disambiguator_input = string * int * 'a type options = { do_heavy_checks: bool ; - clean_baseuri: bool } +(** create a ProofEngineTypes.mk_fresh_name_type function which uses given + * names as long as they are available, then it fallbacks to name generation + * using FreshNamesGenerator module *) +let namer_of names = + let len = List.length names in + let count = ref 0 in + fun metasenv context name ~typ -> + if !count < len then begin + let name = match List.nth names !count with + | Some s -> Cic.Name s + | None -> Cic.Anonymous + in + incr count; + name + end else + FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ + let rec tactic_of_ast status ast = let module PET = ProofEngineTypes in match ast with @@ -75,7 +90,7 @@ let rec tactic_of_ast status ast = Tactics.auto ~params ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe | GrafiteAst.Cases (_, what, (howmany, names)) -> - Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(PEH.namer_of names) + Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names) what | GrafiteAst.Change (_, pattern, with_what) -> Tactics.change ~pattern with_what @@ -83,24 +98,25 @@ let rec tactic_of_ast status ast = | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id | GrafiteAst.Compose (_,t1,t2,times,(howmany, names)) -> Tactics.compose times t1 t2 ?howmany - ~mk_fresh_name_callback:(PEH.namer_of names) + ~mk_fresh_name_callback:(namer_of names) | GrafiteAst.Contradiction _ -> Tactics.contradiction | GrafiteAst.Constructor (_, n) -> Tactics.constructor n | GrafiteAst.Cut (_, ident, term) -> let names = match ident with None -> [] | Some id -> [Some id] in - Tactics.cut ~mk_fresh_name_callback:(PEH.namer_of names) term + Tactics.cut ~mk_fresh_name_callback:(namer_of names) term | GrafiteAst.Decompose (_, names) -> - let mk_fresh_name_callback = PEH.namer_of names in + let mk_fresh_name_callback = namer_of names in Tactics.decompose ~mk_fresh_name_callback () - | GrafiteAst.Demodulate _ -> + | GrafiteAst.Demodulate (_, params) -> Tactics.demodulate - ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe - | GrafiteAst.Destruct (_,xterm) -> Tactics.destruct xterm + ~dbd:(LibraryDb.instance ()) ~params + ~universe:status.GrafiteTypes.universe + | GrafiteAst.Destruct (_,xterms) -> Tactics.destruct xterms | GrafiteAst.Elim (_, what, using, pattern, (depth, names)) -> - Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(PEH.namer_of names) + Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) ~pattern what | GrafiteAst.ElimType (_, what, using, (depth, names)) -> - Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(PEH.namer_of names) + Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) what | GrafiteAst.Exact (_, term) -> Tactics.exact term | GrafiteAst.Exists _ -> Tactics.exists @@ -111,7 +127,6 @@ let rec tactic_of_ast status ast = | `Normalize -> PET.const_lazy_reduction (CicReduction.normalize ~delta:false ~subst:[]) - | `Reduce -> PET.const_lazy_reduction ProofEngineReduction.reduce | `Simpl -> PET.const_lazy_reduction ProofEngineReduction.simpl | `Unfold None -> PET.const_lazy_reduction (ProofEngineReduction.unfold ?what:None) @@ -125,28 +140,27 @@ let rec tactic_of_ast status ast = Tactics.fold ~reduction ~term ~pattern | GrafiteAst.Fourier _ -> Tactics.fourier | GrafiteAst.FwdSimpl (_, hyp, names) -> - Tactics.fwd_simpl ~mk_fresh_name_callback:(PEH.namer_of names) + Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~dbd:(LibraryDb.instance ()) hyp | GrafiteAst.Generalize (_,pattern,ident) -> let names = match ident with None -> [] | Some id -> [Some id] in - Tactics.generalize ~mk_fresh_name_callback:(PEH.namer_of names) pattern + Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern | GrafiteAst.IdTac _ -> Tactics.id | GrafiteAst.Intros (_, (howmany, names)) -> PrimitiveTactics.intros_tac ?howmany - ~mk_fresh_name_callback:(PEH.namer_of names) () + ~mk_fresh_name_callback:(namer_of names) () | GrafiteAst.Inversion (_, term) -> Tactics.inversion term | GrafiteAst.LApply (_, linear, how_many, to_what, what, ident) -> let names = match ident with None -> [] | Some id -> [Some id] in - Tactics.lapply ~mk_fresh_name_callback:(PEH.namer_of names) + Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ~linear ?how_many ~to_what what | GrafiteAst.Left _ -> Tactics.left | GrafiteAst.LetIn (loc,term,name) -> - Tactics.letin term ~mk_fresh_name_callback:(PEH.namer_of [Some name]) + Tactics.letin term ~mk_fresh_name_callback:(namer_of [Some name]) | GrafiteAst.Reduce (_, reduction_kind, pattern) -> (match reduction_kind with | `Normalize -> Tactics.normalize ~pattern - | `Reduce -> Tactics.reduce ~pattern | `Simpl -> Tactics.simpl ~pattern | `Unfold what -> Tactics.unfold ~pattern what | `Whd -> Tactics.whd ~pattern) @@ -155,7 +169,7 @@ let rec tactic_of_ast status ast = Tactics.replace ~pattern ~with_what | GrafiteAst.Rewrite (_, direction, t, pattern, names) -> EqualityTactics.rewrite_tac ~direction ~pattern t -(* to be replaced with ~mk_fresh_name_callback:(PEH.namer_of names) *) +(* to be replaced with ~mk_fresh_name_callback:(namer_of names) *) (List.map (function Some s -> s | None -> assert false) names) | GrafiteAst.Right _ -> Tactics.right | GrafiteAst.Ring _ -> Tactics.ring @@ -204,7 +218,6 @@ let classify_tactic tactic = | _ -> false let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal= - let module PEH = ProofEngineHelpers in (* let print_m name metasenv = prerr_endline (">>>>> " ^ name); prerr_endline (CicMetaSubst.ppmetasenv [] metasenv) @@ -394,7 +407,6 @@ type eval_ast = Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> ?do_heavy_checks:bool -> - ?clean_baseuri:bool -> GrafiteTypes.status -> (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement) disambiguator_input -> @@ -466,10 +478,10 @@ let refinement_toolkit = { RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj; } -let eval_coercion status ~add_composites uri arity saturations baseuri = +let eval_coercion status ~add_composites uri arity saturations = let status,compounds = GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity - saturations baseuri + saturations (GrafiteTypes.get_baseuri status) in let moo_content = List.map coercion_moo_statement_of ((uri,arity,saturations)::compounds) @@ -554,6 +566,7 @@ let add_coercions_of_record_to_moo obj lemmas status = with Not_found -> false,0 with Not_found -> assert false in + let buri = GrafiteTypes.get_baseuri status in (* looking at the fields we can know the 'wanted' coercions, but not the * actually generated ones. So, only the intersection between the wanted * and the actual should be in the moo as coercion, while everithing in @@ -563,8 +576,7 @@ let add_coercions_of_record_to_moo obj lemmas status = (function | (name,true,arity) -> Some - (arity, UriManager.uri_of_string - (GrafiteTypes.qualify status name ^ ".con")) + (arity, UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con" )) | _ -> None) fields in @@ -633,8 +645,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let status = GrafiteTypes.add_moo_content [cmd] status in status,[] | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) -> - eval_coercion status ~add_composites uri arity saturations - (GrafiteTypes.get_string_option status "baseuri") + eval_coercion status ~add_composites uri arity saturations | GrafiteAst.Default (loc, what, uris) as cmd -> LibraryObjects.set_default what uris; GrafiteTypes.add_moo_content [cmd] status,[] @@ -669,7 +680,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status status,[] | GrafiteAst.Print (_,"proofterm") -> let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in - print_endline (Auto.pp_proofterm p); + prerr_endline (Auto.pp_proofterm p); status,[] | GrafiteAst.Print (_,_) -> status,[] | GrafiteAst.Qed loc -> @@ -699,37 +710,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> Setoids.add_relation id a aeq refl sym trans; status, [] (*CSC: TO BE FIXED *) - | GrafiteAst.Set (loc, name, value) -> - if name = "baseuri" then begin - let value = - let v = Http_getter_misc.strip_trailing_slash value in - try - ignore (String.index v ' '); - GrafiteTypes.command_error "baseuri can't contain spaces" - with Not_found -> v - in - if Http_getter_storage.is_read_only value then begin - HLog.error (Printf.sprintf "uri %s belongs to a read-only repository" value); - raise (ReadOnlyUri value) - end; - if (not (Http_getter_storage.is_empty ~local:true value) || - LibraryClean.db_uris_of_baseuri value <> []) - && opts.clean_baseuri - then begin - HLog.message ("baseuri " ^ value ^ " is not empty"); - HLog.message ("cleaning baseuri " ^ value); - LibraryClean.clean_baseuris [value]; - assert (Http_getter_storage.is_empty ~local:true value); - end; - if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk" - ~default:false) - then - HExtlib.mkdir - (Filename.dirname - (Http_getter.filename ~local:true ~writable:true (value ^ - "/foo.con"))); - end; - GrafiteTypes.set_option status name value,[] + | GrafiteAst.Set (loc, name, value) -> status, [] +(* GrafiteTypes.set_option status name value,[] *) | GrafiteAst.Obj (loc,obj) -> let ext,name = match obj with @@ -739,8 +721,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status ".ind", (match types with (name,_,_,_)::_ -> name | _ -> assert false) | _ -> assert false in - let uri = - UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ext) in + let buri = GrafiteTypes.get_baseuri status in + let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ext) in let obj = CicRefine.pack_coercion_obj obj in let metasenv = GrafiteTypes.get_proof_metasenv status in match obj with @@ -844,13 +826,10 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status status) status moo } and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command -~disambiguate_macro ?(do_heavy_checks=false) ?(clean_baseuri=true) status +~disambiguate_macro ?(do_heavy_checks=false) status (text,prefix_len,st) -> - let opts = { - do_heavy_checks = do_heavy_checks ; - clean_baseuri = clean_baseuri } - in + let opts = { do_heavy_checks = do_heavy_checks ; } in match st with | GrafiteAst.Executable (_,ex) -> eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command