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
| GrafiteAst.AutoBatch (_,params) ->
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)
- what
+ | GrafiteAst.Cases (_, what, pattern, (howmany, names)) ->
+ Tactics.cases_intros ?howmany ~mk_fresh_name_callback:(namer_of names)
+ ~pattern what
| GrafiteAst.Change (_, pattern, with_what) ->
Tactics.change ~pattern with_what
| GrafiteAst.Clear (_,id) -> Tactics.clear id
| 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
| `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)
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)
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
(* Implementazioni Aggiunte *)
| GrafiteAst.Assume (_, id, t) -> Declarative.assume id t
| GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1
- | GrafiteAst.By_term_we_proved (_, t, ty, id, t1) ->
- Declarative.by_term_we_proved ~dbd:(LibraryDb.instance())
- ~universe:status.GrafiteTypes.universe t ty id t1
+ | GrafiteAst.By_just_we_proved (_, just, ty, id, t1) ->
+ Declarative.by_just_we_proved ~dbd:(LibraryDb.instance())
+ ~universe:status.GrafiteTypes.universe just ty id t1
| GrafiteAst.We_need_to_prove (_, t, id, t2) ->
Declarative.we_need_to_prove t id t2
| GrafiteAst.Bydone (_, t) ->
Declarative.we_proceed_by_induction_on t t1
| GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction t id
| GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t
- | GrafiteAst.ExistsElim (_, t, id1, t1, id2, t2) ->
+ | GrafiteAst.ExistsElim (_, just, id1, t1, id2, t2) ->
Declarative.existselim ~dbd:(LibraryDb.instance())
- ~universe:status.GrafiteTypes.universe t id1 t1 id2 t2
+ ~universe:status.GrafiteTypes.universe just 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.AndElim(_,just,id1,t1,id2,t2) ->
+ Declarative.andelim ~dbd:(LibraryDb.instance ())
+ ~universe:status.GrafiteTypes.universe just id1 t1 id2 t2
| GrafiteAst.RewritingStep (_,termine,t1,t2,cont) ->
Declarative.rewritingstep ~dbd:(LibraryDb.instance ())
~universe:status.GrafiteTypes.universe termine t1 t2 cont
| _ -> 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)
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 ->
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)
let is_a_coercion uri =
try
let obj,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
+ CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri in
let attrs = CicUtil.attributes_of_obj obj in
try
match List.find
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
(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
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,[]
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 ->
| 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
".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
let t = CicUtil.term_of_uri u in
let ty',g =
CicTypeChecker.type_of_aux'
- metasenv' [] t CicUniv.empty_ugraph
+ metasenv' [] t CicUniv.oblivion_ugraph
in
fst(CicReduction.are_convertible [] ty' ty g))
similar
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
projects / helm.git / blobdiff