X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=7cf3897faf2ffe697a7e2df1c03228e57de783bc;hb=912780aaffd1e3a107a837dac1443ad2476e94b7;hp=43906f8cd43266ca422955c375a084d38f52e9c2;hpb=3b8d99d5fdb79a5d979a8e200a4a4307fe362009;p=helm.git diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 43906f8cd..7cf3897fa 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -32,7 +32,7 @@ exception Drop exception IncludedFileNotCompiled of string * string exception Macro of GrafiteAst.loc * - (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) + (Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) type 'a disambiguator_input = string * int * 'a @@ -82,6 +82,7 @@ let rec tactic_of_ast status ast = (* First order tactics *) | GrafiteAst.Absurd (_, term) -> Tactics.absurd term | GrafiteAst.Apply (_, term) -> Tactics.apply term + | GrafiteAst.ApplyRule (_, term) -> Tactics.apply term | GrafiteAst.ApplyP (_, term) -> Tactics.applyP term | GrafiteAst.ApplyS (_, term, params) -> Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ()) @@ -406,8 +407,8 @@ type eval_ast = disambiguate_macro: (GrafiteTypes.status -> - ('term GrafiteAst.macro) disambiguator_input -> - Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> + (('term,'lazy_term) GrafiteAst.macro) disambiguator_input -> + Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) -> ?do_heavy_checks:bool -> GrafiteTypes.status -> @@ -426,6 +427,16 @@ type 'a eval_command = GrafiteTypes.status * UriManager.uri list } +type 'a eval_comment = + {ecm_go: 'term 'lazy_term 'reduction_kind 'obj 'ident. + disambiguate_command: + (GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input -> + GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> + options -> GrafiteTypes.status -> + (('term,'lazy_term,'reduction_kind,'obj,'ident) GrafiteAst.comment) disambiguator_input -> + GrafiteTypes.status * UriManager.uri list + } + type 'a eval_executable = {ee_go: 'term 'lazy_term 'reduction 'obj 'ident. disambiguate_tactic: @@ -443,8 +454,8 @@ type 'a eval_executable = disambiguate_macro: (GrafiteTypes.status -> - ('term GrafiteAst.macro) disambiguator_input -> - Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> + (('term,'lazy_term) GrafiteAst.macro) disambiguator_input -> + Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) -> options -> GrafiteTypes.status -> @@ -455,7 +466,7 @@ type 'a eval_executable = type 'a eval_from_moo = { efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status } -let coercion_moo_statement_of (uri,arity, saturations) = +let coercion_moo_statement_of (uri,arity, saturations,_) = GrafiteAst.Coercion (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations) @@ -481,7 +492,13 @@ let refinement_toolkit = { RefinementTool.ppmetasenv = CicMetaSubst.ppmetasenv; RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj; } - + +let eval_unification_hint status t = + (* XXX no undo *) + NCicUnifHint.add_user_provided_hint t; + status,[] +;; + let eval_coercion status ~add_composites uri arity saturations = let uri = try CicUtil.uri_of_term uri @@ -493,11 +510,11 @@ let eval_coercion status ~add_composites uri arity saturations = saturations (GrafiteTypes.get_baseuri status) in let moo_content = - List.map coercion_moo_statement_of ((uri,arity,saturations)::compounds) + List.map coercion_moo_statement_of ((uri,arity,saturations,0)::compounds) in let status = GrafiteTypes.add_moo_content moo_content status in {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, - List.map (fun u,_,_ -> u) compounds + List.map (fun u,_,_,_ -> u) compounds module MatitaStatus = struct @@ -553,13 +570,11 @@ let eval_tactical status tac = in status -let eval_comment status c = status - (* since the record syntax allows to declare coercions, we have to put this * information inside the moo *) let add_coercions_of_record_to_moo obj lemmas status = let attributes = CicUtil.attributes_of_obj obj in - let is_record = function `Class (`Record att) -> Some att | _-> None in + let is_record x _ = match x with `Class (`Record att) -> Some att | _-> None in match HExtlib.list_findopt is_record attributes with | None -> status,[] | Some fields -> @@ -608,9 +623,9 @@ let add_coercions_of_record_to_moo obj lemmas status = in let is_a_coercion, arity_coercion = is_a_coercion uri in if is_a_coercion then - Some (uri, coercion_moo_statement_of (uri,arity_coercion,0)) + Some (uri, coercion_moo_statement_of (uri,arity_coercion,0,0)) else if is_a_wanted_coercion then - Some (uri, coercion_moo_statement_of (uri,arity_wanted,0)) + Some (uri, coercion_moo_statement_of (uri,arity_wanted,0,0)) else None) lemmas) @@ -655,6 +670,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status status,[] | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) -> eval_coercion status ~add_composites uri arity saturations + | GrafiteAst.UnificationHint (loc, t) -> + eval_unification_hint status t | GrafiteAst.Default (loc, what, uris) as cmd -> LibraryObjects.set_default what uris; GrafiteTypes.add_moo_content [cmd] status,[] @@ -689,7 +706,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status status,[] | GrafiteAst.Print (_,"proofterm") -> let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in - prerr_endline (Auto.pp_proofterm p); + prerr_endline (Auto.pp_proofterm (Lazy.force p)); status,[] | GrafiteAst.Print (_,_) -> status,[] | GrafiteAst.Qed loc -> @@ -710,7 +727,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,[],attrs) in + let obj = Cic.Constant (name,Some (Lazy.force bo),ty,[],attrs) in let status, lemmas = add_obj uri obj status in {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, @@ -768,7 +785,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status "\nPlease use a variant.")); end; let _subst = [] in - let initial_proof = (Some uri, metasenv', _subst, bo, ty, attrs) in + let initial_proof = (Some uri, metasenv', _subst, lazy bo, ty, attrs) in let initial_stack = Continuationals.Stack.of_metasenv metasenv' in { status with GrafiteTypes.proof_status = GrafiteTypes.Incomplete_proof @@ -794,9 +811,18 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status } and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command ~disambiguate_macro opts status (text,prefix_len,ex) -> match ex with - | GrafiteAst.Tactic (_, Some tac, punct) -> + | GrafiteAst.Tactic (_(*loc*), Some tac, punct) -> let tac = apply_tactic ~disambiguate_tactic (text,prefix_len,tac) in let status = eval_tactical status (tactic_of_ast' tac) in + (* CALL auto on every goal, easy way of testing it + let auto = + GrafiteAst.AutoBatch + (loc, ([],["depth","2";"timeout","1";"type","1"])) in + (try + let auto = apply_tactic ~disambiguate_tactic ("",0,auto) in + let _ = eval_tactical status (tactic_of_ast' auto) in + print_endline "GOOD"; () + with ProofEngineTypes.Fail _ -> print_endline "BAD" | _ -> ());*) eval_tactical status (punctuation_tactical_of_ast (text,prefix_len,punct)),[] | GrafiteAst.Tactic (_, None, punct) -> @@ -843,7 +869,12 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status | GrafiteAst.Executable (_,ex) -> eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command ~disambiguate_macro opts status (text,prefix_len,ex) - | GrafiteAst.Comment (_,c) -> eval_comment status (text,prefix_len,c),[] + | GrafiteAst.Comment (_,c) -> + eval_comment.ecm_go ~disambiguate_command opts status (text,prefix_len,c) +} and eval_comment = { ecm_go = fun ~disambiguate_command opts status (text,prefix_len,c) -> + status, [] } +;; + let eval_ast = eval_ast.ea_go