X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=f58f4303c2ada346206ac1fb31c77312581be168;hb=84e770b58ae08a345087de816aba29bc2fc727ba;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..f58f4303c 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 -> @@ -443,8 +444,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 +456,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) @@ -493,11 +494,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 @@ -559,7 +560,7 @@ let eval_comment status c = status * 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 +609,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) @@ -689,7 +690,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 +711,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 +769,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 +795,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) ->