X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=f0d8ee46c7820b34feff186135edcd418b9b4fd4;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=3c54f5a1b6730510751e2e96a88d331c38b163fc;hpb=4658fcc5315ff90510a0e6ff7790156092ec44ce;p=helm.git diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 3c54f5a1b..f0d8ee46c 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -23,754 +23,120 @@ * http://helm.cs.unibo.it/ *) -open Printf -open MatitaTypes +(* $Id$ *) -exception Drop;; -exception UnableToInclude of string -exception IncludedFileNotCompiled of string +open Printf let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; -type options = { - do_heavy_checks: bool ; - include_paths: string list ; - clean_baseuri: bool -} - -type statement = - (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement - -(** 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 = Cic.Name (List.nth names !count) in - incr count; - name - end else - FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ - -let tactic_of_ast = function - | GrafiteAst.Absurd (_, term) -> Tactics.absurd term - | GrafiteAst.Apply (_, term) -> Tactics.apply term - | GrafiteAst.Assumption _ -> Tactics.assumption - | GrafiteAst.Auto (_,depth,width,paramodulation) -> (* ALB *) - AutoTactic.auto_tac ?depth ?width ?paramodulation - ~dbd:(MatitaDb.instance ()) () - | GrafiteAst.Change (_, pattern, with_what) -> - Tactics.change ~pattern with_what - | GrafiteAst.Clear (_,id) -> Tactics.clear id - | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id - | GrafiteAst.Contradiction _ -> Tactics.contradiction - | GrafiteAst.Compare (_, term) -> Tactics.compare term - | GrafiteAst.Constructor (_, n) -> Tactics.constructor n - | 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.DecideEquality _ -> Tactics.decide_equality - | GrafiteAst.Decompose (_, types, what, names) -> - let to_type = function - | GrafiteAst.Type (uri, typeno) -> uri, typeno - | GrafiteAst.Ident _ -> assert false - in - let user_types = List.rev_map to_type types in - let dbd = MatitaDb.instance () in - let mk_fresh_name_callback = namer_of names in - Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what - | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term - | GrafiteAst.Elim (_, what, using, depth, names) -> - Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) what - | GrafiteAst.ElimType (_, what, using, depth, names) -> - Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) what - | GrafiteAst.Exact (_, term) -> Tactics.exact term - | GrafiteAst.Exists _ -> Tactics.exists - | GrafiteAst.Fail _ -> Tactics.fail - | GrafiteAst.Fold (_, reduction_kind, term, pattern) -> - let reduction = - match reduction_kind with - | `Normalize -> CicReduction.normalize ~delta:false ~subst:[] - | `Reduce -> ProofEngineReduction.reduce - | `Simpl -> ProofEngineReduction.simpl - | `Unfold what -> ProofEngineReduction.unfold ?what - | `Whd -> CicReduction.whd ~delta:false ~subst:[] - in - Tactics.fold ~reduction ~term ~pattern - | GrafiteAst.Fourier _ -> Tactics.fourier - | GrafiteAst.FwdSimpl (_, hyp, names) -> - Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~dbd:(MatitaDb.instance ()) hyp - | GrafiteAst.Generalize (_,pattern,ident) -> - let names = match ident with None -> [] | Some id -> [id] in - Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern - | GrafiteAst.Goal (_, n) -> Tactics.set_goal n - | GrafiteAst.IdTac _ -> Tactics.id - | GrafiteAst.Injection (_,term) -> Tactics.injection term - | GrafiteAst.Intros (_, None, names) -> - PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () - | GrafiteAst.Intros (_, Some num, names) -> - PrimitiveTactics.intros_tac ~howmany:num - ~mk_fresh_name_callback:(namer_of names) () - | GrafiteAst.LApply (_, how_many, to_what, what, ident) -> - let names = match ident with None -> [] | Some id -> [id] in - Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many ~to_what what - | GrafiteAst.Left _ -> Tactics.left - | GrafiteAst.LetIn (loc,term,name) -> - Tactics.letin term ~mk_fresh_name_callback:(namer_of [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) - | GrafiteAst.Reflexivity _ -> Tactics.reflexivity - | GrafiteAst.Replace (_, pattern, with_what) -> - Tactics.replace ~pattern ~with_what - | GrafiteAst.Rewrite (_, direction, t, pattern) -> - EqualityTactics.rewrite_tac ~direction ~pattern t - | GrafiteAst.Right _ -> Tactics.right - | GrafiteAst.Ring _ -> Tactics.ring - | GrafiteAst.Split _ -> Tactics.split - | GrafiteAst.Symmetry _ -> Tactics.symmetry - | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term - -let disambiguate_term status term = - let (aliases, metasenv, cic, _) = - match - MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ()) - ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status) - ~metasenv:(MatitaMisc.get_proof_metasenv status) term - with - | [x] -> x - | _ -> assert false - in - let proof_status = - match status.proof_status with - | No_proof -> Intermediate metasenv - | Incomplete_proof ((uri, _, proof, ty), goal) -> - Incomplete_proof ((uri, metasenv, proof, ty), goal) - | Intermediate _ -> Intermediate metasenv - | Proof _ -> assert false - in - let status = { status with proof_status = proof_status } in - let status = MatitaSync.set_proof_aliases status aliases in - status, cic - -let disambiguate_pattern status (wanted, hyp_paths, goal_path) = - let interp path = Disambiguate.interpretate_path [] status.aliases path in - let goal_path = interp goal_path in - let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in - let status,wanted = - match wanted with - None -> status,None - | Some wanted -> - let status,wanted = disambiguate_term status wanted in - status, Some wanted - in - status, (wanted, hyp_paths ,goal_path) - -let disambiguate_reduction_kind status = function - | `Unfold (Some t) -> - let status, t = disambiguate_term status t in - status, `Unfold (Some t) - | `Normalize - | `Reduce - | `Simpl - | `Unfold None - | `Whd as kind -> status, kind - -let disambiguate_tactic status = function - | GrafiteAst.Apply (loc, term) -> - let status, cic = disambiguate_term status term in - status, GrafiteAst.Apply (loc, cic) - | GrafiteAst.Absurd (loc, term) -> - let status, cic = disambiguate_term status term in - status, GrafiteAst.Absurd (loc, cic) - | GrafiteAst.Assumption loc -> status, GrafiteAst.Assumption loc - | GrafiteAst.Auto (loc,depth,width,paramodulation) -> status, GrafiteAst.Auto (loc,depth,width,paramodulation) (* ALB *) - | GrafiteAst.Change (loc, pattern, with_what) -> - let status, with_what = disambiguate_term status with_what in - let status, pattern = disambiguate_pattern status pattern in - status, GrafiteAst.Change (loc, pattern, with_what) - | GrafiteAst.Clear (loc,id) -> status,GrafiteAst.Clear (loc,id) - | GrafiteAst.ClearBody (loc,id) -> status,GrafiteAst.ClearBody (loc,id) - | GrafiteAst.Compare (loc,term) -> - let status, term = disambiguate_term status term in - status, GrafiteAst.Compare (loc,term) - | GrafiteAst.Constructor (loc,n) -> - status, GrafiteAst.Constructor (loc,n) - | GrafiteAst.Contradiction loc -> - status, GrafiteAst.Contradiction loc - | GrafiteAst.Cut (loc, ident, term) -> - let status, cic = disambiguate_term status term in - status, GrafiteAst.Cut (loc, ident, cic) - | GrafiteAst.DecideEquality loc -> - status, GrafiteAst.DecideEquality loc - | GrafiteAst.Decompose (loc, types, what, names) -> - let disambiguate (status, types) = function - | GrafiteAst.Type _ -> assert false - | GrafiteAst.Ident id -> - match disambiguate_term status (CicNotationPt.Ident (id, None)) with - | status, Cic.MutInd (uri, tyno, _) -> - status, (GrafiteAst.Type (uri, tyno) :: types) - | _ -> - raise Disambiguate.NoWellTypedInterpretation - in - let status, types = List.fold_left disambiguate (status, []) types in - status, GrafiteAst.Decompose(loc, types, what, names) - | GrafiteAst.Discriminate (loc,term) -> - let status,term = disambiguate_term status term in - status, GrafiteAst.Discriminate(loc,term) - | GrafiteAst.Exact (loc, term) -> - let status, cic = disambiguate_term status term in - status, GrafiteAst.Exact (loc, cic) - | GrafiteAst.Elim (loc, what, Some using, depth, idents) -> - let status, what = disambiguate_term status what in - let status, using = disambiguate_term status using in - status, GrafiteAst.Elim (loc, what, Some using, depth, idents) - | GrafiteAst.Elim (loc, what, None, depth, idents) -> - let status, what = disambiguate_term status what in - status, GrafiteAst.Elim (loc, what, None, depth, idents) - | GrafiteAst.ElimType (loc, what, Some using, depth, idents) -> - let status, what = disambiguate_term status what in - let status, using = disambiguate_term status using in - status, GrafiteAst.ElimType (loc, what, Some using, depth, idents) - | GrafiteAst.ElimType (loc, what, None, depth, idents) -> - let status, what = disambiguate_term status what in - status, GrafiteAst.ElimType (loc, what, None, depth, idents) - | GrafiteAst.Exists loc -> status, GrafiteAst.Exists loc - | GrafiteAst.Fail loc -> status,GrafiteAst.Fail loc - | GrafiteAst.Fold (loc,red_kind, term, pattern) -> - let status, pattern = disambiguate_pattern status pattern in - let status, term = disambiguate_term status term in - let status, red_kind = disambiguate_reduction_kind status red_kind in - status, GrafiteAst.Fold (loc,red_kind, term, pattern) - | GrafiteAst.FwdSimpl (loc, hyp, names) -> - status, GrafiteAst.FwdSimpl (loc, hyp, names) - | GrafiteAst.Fourier loc -> status, GrafiteAst.Fourier loc - | GrafiteAst.Generalize (loc,pattern,ident) -> - let status, pattern = disambiguate_pattern status pattern in - status, GrafiteAst.Generalize(loc,pattern,ident) - | GrafiteAst.Goal (loc, g) -> status, GrafiteAst.Goal (loc, g) - | GrafiteAst.IdTac loc -> status,GrafiteAst.IdTac loc - | GrafiteAst.Injection (loc,term) -> - let status, term = disambiguate_term status term in - status, GrafiteAst.Injection (loc,term) - | GrafiteAst.Intros (loc, num, names) -> - status, GrafiteAst.Intros (loc, num, names) - | GrafiteAst.LApply (loc, depth, to_what, what, ident) -> - let f term (status, to_what) = - let status, term = disambiguate_term status term in - status, term :: to_what - in - let status, to_what = List.fold_right f to_what (status, []) in - let status, what = disambiguate_term status what in - status, GrafiteAst.LApply (loc, depth, to_what, what, ident) - | GrafiteAst.Left loc -> status, GrafiteAst.Left loc - | GrafiteAst.LetIn (loc, term, name) -> - let status, term = disambiguate_term status term in - status, GrafiteAst.LetIn (loc,term,name) - | GrafiteAst.Reduce (loc, red_kind, pattern) -> - let status, pattern = disambiguate_pattern status pattern in - let status, red_kind = disambiguate_reduction_kind status red_kind in - status, GrafiteAst.Reduce(loc, red_kind, pattern) - | GrafiteAst.Reflexivity loc -> status, GrafiteAst.Reflexivity loc - | GrafiteAst.Replace (loc, pattern, with_what) -> - let status, pattern = disambiguate_pattern status pattern in - let status, with_what = disambiguate_term status with_what in - status, GrafiteAst.Replace (loc, pattern, with_what) - | GrafiteAst.Rewrite (loc, dir, t, pattern) -> - let status, term = disambiguate_term status t in - let status, pattern = disambiguate_pattern status pattern in - status, GrafiteAst.Rewrite (loc, dir, term, pattern) - | GrafiteAst.Right loc -> status, GrafiteAst.Right loc - | GrafiteAst.Ring loc -> status, GrafiteAst.Ring loc - | GrafiteAst.Split loc -> status, GrafiteAst.Split loc - | GrafiteAst.Symmetry loc -> status, GrafiteAst.Symmetry loc - | GrafiteAst.Transitivity (loc, term) -> - let status, cic = disambiguate_term status term in - status, GrafiteAst.Transitivity (loc, cic) - -let apply_tactic tactic status = - let status,tactic = disambiguate_tactic status tactic in - let tactic = tactic_of_ast tactic in - let (proof, goals) = - ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status) in - let dummy = -1 in - { status with - proof_status = MatitaTypes.Incomplete_proof (proof,dummy) }, goals - -module MatitaStatus = - struct - type input_status = MatitaTypes.status - type output_status = MatitaTypes.status * ProofEngineTypes.goal list - type tactic = input_status -> output_status - - let focus (status,_) goal = - let proof,_ = MatitaMisc.get_proof_status status in - {status with proof_status = MatitaTypes.Incomplete_proof (proof,goal)} - - let goals (_,goals) = goals - - let set_goals (status,_) goals = status,goals - - let id_tac status = - apply_tactic (GrafiteAst.IdTac Disambiguate.dummy_floc) status - - let mk_tactic tac = tac - - let apply_tactic tac = tac - - end - -module MatitaTacticals = Tacticals.Make(MatitaStatus) - -let eval_tactical status tac = - let rec tactical_of_ast tac = - match tac with - | GrafiteAst.Tactic (loc, tactic) -> apply_tactic tactic - | GrafiteAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *) - MatitaTacticals.seq ~tactics:(List.map tactical_of_ast tacticals) - | GrafiteAst.Do (loc, num, tactical) -> - MatitaTacticals.do_tactic ~n:num ~tactic:(tactical_of_ast tactical) - | GrafiteAst.Repeat (loc, tactical) -> - MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast tactical) - | GrafiteAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *) - MatitaTacticals.thens ~start:(tactical_of_ast tactical) - ~continuations:(List.map tactical_of_ast tacticals) - | GrafiteAst.First (loc, tacticals) -> - MatitaTacticals.first - ~tactics:(List.map (fun t -> "", tactical_of_ast t) tacticals) - | GrafiteAst.Try (loc, tactical) -> - MatitaTacticals.try_tactic ~tactic:(tactical_of_ast tactical) - | GrafiteAst.Solve (loc, tacticals) -> - MatitaTacticals.solve_tactics - ~tactics:(List.map (fun t -> "",tactical_of_ast t) tacticals) +let disambiguate_tactic lexicon_status_ref grafite_status goal tac = + let metasenv,tac = + GrafiteDisambiguate.disambiguate_tactic + lexicon_status_ref + (GrafiteTypes.get_proof_context grafite_status goal) + (GrafiteTypes.get_proof_metasenv grafite_status) + tac in - let status,goals = tactical_of_ast tac status in - let proof,_ = MatitaMisc.get_proof_status status in - let new_status = - match goals with - | [] -> - let (_,metasenv,_,_) = proof in - (match metasenv with - | [] -> Proof proof - | (ng,_,_)::_ -> Incomplete_proof (proof,ng)) - | ng::_ -> Incomplete_proof (proof, ng) - in - { status with proof_status = new_status } - -let eval_coercion status coercion = - let coer_uri,coer_ty = - match coercion with - | Cic.Const (uri,_) - | Cic.Var (uri,_) -> - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - (match o with - | Cic.Constant (_,_,ty,_,_) - | Cic.Variable (_,_,ty,_,_) -> - uri,ty - | _ -> assert false) - | Cic.MutConstruct (uri,t,c,_) -> - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - (match o with - | Cic.InductiveDefinition (l,_,_,_) -> - let (_,_,_,cl) = List.nth l t in - let (_,cty) = List.nth cl c in - uri,cty - | _ -> assert false) - | _ -> assert false - in - (* we have to get the source and the tgt type uri - * in Coq syntax we have already their names, but - * since we don't support Funclass and similar I think - * all the coercion should be of the form - * (A:?)(B:?)T1->T2 - * So we should be able to extract them from the coercion type - *) - let extract_last_two_p ty = - let rec aux = function - | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2)) - | Cic.Prod( _, src, tgt) -> src, tgt - | _ -> assert false - in - aux ty - in - let ty_src,ty_tgt = extract_last_two_p coer_ty in - let context = [] in - let src_uri = - let ty_src = CicReduction.whd context ty_src in - CicUtil.uri_of_term ty_src - in - let tgt_uri = - let ty_tgt = CicReduction.whd context ty_tgt in - CicUtil.uri_of_term ty_tgt - in - let new_coercions = - (* also adds them to the Db *) - CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in - let status = - List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status) - status new_coercions in - let statement_of name = - GrafiteAstPp.pp_statement - (GrafiteAst.Executable (Disambiguate.dummy_floc, - (GrafiteAst.Command (Disambiguate.dummy_floc, - (GrafiteAst.Coercion (Disambiguate.dummy_floc, - (CicNotationPt.Ident (name, None)))))))) ^ "\n" - in - let moo_content_rev = - [statement_of (UriManager.name_of_uri coer_uri)] @ - (List.map - (fun (uri, _, _) -> - statement_of (UriManager.name_of_uri uri)) - new_coercions) @ status.moo_content_rev - in - let status = {status with moo_content_rev = moo_content_rev} in - {status with proof_status = No_proof} - -let generate_elimination_principles uri status = - let elim sort status = - try - let uri,obj = CicElim.elim_of ~sort uri 0 in - MatitaSync.add_obj uri obj status - with CicElim.Can_t_eliminate -> status + GrafiteTypes.set_metasenv metasenv grafite_status,tac + +let disambiguate_command lexicon_status_ref grafite_status cmd = + let lexicon_status,metasenv,cmd = + GrafiteDisambiguate.disambiguate_command + ~baseuri:( + try + Some (GrafiteTypes.get_string_option grafite_status "baseuri") + with + GrafiteTypes.Option_error _ -> None) + !lexicon_status_ref (GrafiteTypes.get_proof_metasenv grafite_status) cmd + in + lexicon_status_ref := lexicon_status; + GrafiteTypes.set_metasenv metasenv grafite_status,cmd + +let disambiguate_macro lexicon_status_ref grafite_status macro context = + let metasenv,macro = + GrafiteDisambiguate.disambiguate_macro + lexicon_status_ref + (GrafiteTypes.get_proof_metasenv grafite_status) + context macro in - List.fold_left (fun status sort -> elim sort status) status - [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ] + GrafiteTypes.set_metasenv metasenv grafite_status,macro -let generate_projections uri fields status = - let projections = CicRecord.projections_of uri fields in +let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status + grafite_status ast += + let lexicon_status_ref = ref lexicon_status in + let new_grafite_status,new_objs = + GrafiteEngine.eval_ast + ~disambiguate_tactic:(disambiguate_tactic lexicon_status_ref) + ~disambiguate_command:(disambiguate_command lexicon_status_ref) + ~disambiguate_macro:(disambiguate_macro lexicon_status_ref) + ?do_heavy_checks ?clean_baseuri grafite_status ast in + let new_lexicon_status = + LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs in + let new_aliases = + LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in + let _,intermediate_states = + let baseuri = GrafiteTypes.get_string_option new_grafite_status "baseuri" in List.fold_left - (fun status (uri, name, bo) -> - try - let ty, ugraph = - CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in - let attrs = [`Class `Projection; `Generated] in - let obj = Cic.Constant (name,Some bo,ty,[],attrs) in - MatitaSync.add_obj uri obj status - with - CicTypeChecker.TypeCheckerFailure s -> - MatitaLog.message - ("Unable to create projection " ^ name ^ " cause: " ^ s); - status - | CicEnvironment.Object_not_found uri -> - let depend = UriManager.name_of_uri uri in - MatitaLog.message - ("Unable to create projection " ^ name ^ " because it requires " ^ depend); - status - ) status projections - -(* to avoid a long list of recursive functions *) -let eval_from_stream_ref = ref (fun _ _ _ -> assert false);; - -let disambiguate_obj status obj = - let uri = - match obj with - GrafiteAst.Inductive (_,(name,_,_,_)::_) - | GrafiteAst.Record (_,name,_,_) -> - Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind")) - | GrafiteAst.Inductive _ -> assert false - | GrafiteAst.Theorem _ -> None in - let (aliases, metasenv, cic, _) = - match - MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ()) - ~aliases:(status.aliases) ~uri obj - with - | [x] -> x - | _ -> assert false - in - let proof_status = - match status.proof_status with - | No_proof -> Intermediate metasenv - | Incomplete_proof _ - | Intermediate _ - | Proof _ -> assert false - in - let status = { status with proof_status = proof_status } in - let status = MatitaSync.set_proof_aliases status aliases in - status, cic - -let disambiguate_command status = function - | GrafiteAst.Alias _ - | GrafiteAst.Default _ - | GrafiteAst.Drop _ - | GrafiteAst.Dump _ - | GrafiteAst.Include _ - | GrafiteAst.Interpretation _ - | GrafiteAst.Notation _ - | GrafiteAst.Qed _ - | GrafiteAst.Render _ - | GrafiteAst.Set _ as cmd -> - status,cmd - | GrafiteAst.Coercion (loc, term) -> - let status, term = disambiguate_term status term in - status, GrafiteAst.Coercion (loc,term) - | GrafiteAst.Obj (loc,obj) -> - let status,obj = disambiguate_obj status obj in - status, GrafiteAst.Obj (loc,obj) - -let make_absolute paths path = - if path = "coq.ma" then path - else - let rec aux = function - | [] -> ignore (Unix.stat path); path - | p :: tl -> - let path = p ^ "/" ^ path in - try - ignore (Unix.stat path); path - with Unix.Unix_error _ -> aux tl - in - try - aux paths - with Unix.Unix_error _ as exc -> raise (UnableToInclude path) -;; - -let eval_command opts status cmd = - let status,cmd = disambiguate_command status cmd in - let cmd,notation_ids' = CicNotation.process_notation cmd in - let status = - { status with notation_ids = notation_ids' @ status.notation_ids } - in - match cmd with - | GrafiteAst.Default (loc, what, uris) as cmd -> - LibraryObjects.set_default what uris; - {status with moo_content_rev = - (GrafiteAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev} - | GrafiteAst.Include (loc, path) -> - let absolute_path = make_absolute opts.include_paths path in - let moopath = MatitaMisc.obj_file_of_script absolute_path in - let ic = - try open_in moopath with Sys_error _ -> - raise (IncludedFileNotCompiled moopath) in - let stream = Stream.of_channel ic in - let status = ref status in - !eval_from_stream_ref status stream (fun _ _ -> ()); - close_in ic; - !status - | GrafiteAst.Set (loc, name, value) -> - let value = - if name = "baseuri" then - let v = MatitaMisc.strip_trailing_slash value in - try - ignore (String.index v ' '); - command_error "baseuri can't contain spaces" - with Not_found -> v - else - value - in - if not (MatitaMisc.is_empty value) then - begin - MatitaLog.warn ("baseuri " ^ value ^ " is not empty"); - if opts.clean_baseuri then - begin - MatitaLog.message ("cleaning baseuri " ^ value); - MatitacleanLib.clean_baseuris [value] - end - end; - set_option status name value - | GrafiteAst.Drop loc -> raise Drop - | GrafiteAst.Qed loc -> - let uri, metasenv, bo, ty = - match status.proof_status with - | Proof (Some uri, metasenv, body, ty) -> - uri, metasenv, body, ty - | Proof (None, metasenv, body, ty) -> - command_error - ("Someone allows to start a thm without giving the "^ - "name/uri. This should be fixed!") - | _-> command_error "You can't qed an uncomplete theorem" - in - let suri = UriManager.string_of_uri uri in - if metasenv <> [] then - 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 - MatitaSync.add_obj uri obj status - | GrafiteAst.Coercion (loc, coercion) -> - eval_coercion status coercion - | GrafiteAst.Alias (loc, spec) -> - let aliases = - (*CSC: Warning: this code should be factorized with the corresponding - code in DisambiguatePp *) - match spec with - | GrafiteAst.Ident_alias (id,uri) -> - DisambiguateTypes.Environment.add - (DisambiguateTypes.Id id) - (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri))) - status.aliases - | GrafiteAst.Symbol_alias (symb, instance, desc) -> - DisambiguateTypes.Environment.add - (DisambiguateTypes.Symbol (symb,instance)) - (DisambiguateChoices.lookup_symbol_by_dsc symb desc) - status.aliases - | GrafiteAst.Number_alias (instance,desc) -> - DisambiguateTypes.Environment.add - (DisambiguateTypes.Num instance) - (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases - in - MatitaSync.set_proof_aliases status aliases - | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *) - | GrafiteAst.Dump _ -> assert false (* ZACK: to be removed *) - | GrafiteAst.Interpretation _ - | GrafiteAst.Notation _ as stm -> - { status with moo_content_rev = - (GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev } - | GrafiteAst.Obj (loc,obj) -> - let ext,name = - match obj with - Cic.Constant (name,_,_,_,_) - | Cic.CurrentProof (name,_,_,_,_,_) -> ".con",name - | Cic.InductiveDefinition (types,_,_,_) -> - ".ind", - (match types with (name,_,_,_)::_ -> name | _ -> assert false) - | _ -> assert false in - let uri = - UriManager.uri_of_string (MatitaMisc.qualify status name ^ ext) + (fun (lexicon_status,acc) (k,((v,_) as value)) -> + let b = + try + UriManager.buri_of_uri (UriManager.uri_of_string v) = baseuri + with + UriManager.IllFormedUri _ -> false (* v is a description, not a URI *) in - let metasenv = MatitaMisc.get_proof_metasenv status in - match obj with - | Cic.CurrentProof (_,metasenv',bo,ty,_,_) -> - let name = UriManager.name_of_uri uri in - if not(CicPp.check name ty) then - MatitaLog.error ("Bad name: " ^ name); - if opts.do_heavy_checks then - begin - let dbd = MatitaDb.instance () in - let similar = MetadataQuery.match_term ~dbd ty in - let similar_len = List.length similar in - if similar_len> 30 then - (MatitaLog.message - ("Duplicate check will compare your theorem with " ^ - string_of_int similar_len ^ - " theorems, this may take a while.")); - let convertible = - List.filter ( - fun u -> - let t = CicUtil.term_of_uri u in - let ty',g = - CicTypeChecker.type_of_aux' - metasenv' [] t CicUniv.empty_ugraph - in - fst(CicReduction.are_convertible [] ty' ty g)) - similar - in - (match convertible with - | [] -> () - | x::_ -> - MatitaLog.warn - ("Theorem already proved: " ^ UriManager.string_of_uri x ^ - "\nPlease use a variant.")); - end; - assert (metasenv = metasenv'); - let goalno = - match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false - in - let initial_proof = (Some uri, metasenv, bo, ty) in - { status with proof_status = Incomplete_proof (initial_proof,goalno)} - | _ -> - if metasenv <> [] then - command_error ( - "metasenv not empty while giving a definition with body: " ^ - CicMetaSubst.ppmetasenv metasenv []); - let status = MatitaSync.add_obj uri obj status in - match obj with - Cic.Constant _ -> status - | Cic.InductiveDefinition (_,_,_,attrs) -> - let status = generate_elimination_principles uri status in - let rec get_record_attrs = - function - [] -> None - | (`Class (`Record fields))::_ -> Some fields - | _::tl -> get_record_attrs tl - in - (match get_record_attrs attrs with - None -> status (* not a record *) - | Some fields -> generate_projections uri fields status) - | Cic.CurrentProof _ - | Cic.Variable _ -> assert false - -let eval_executable opts status ex = - match ex with - | GrafiteAst.Tactical (_, tac) -> eval_tactical status tac - | GrafiteAst.Command (_, cmd) -> eval_command opts status cmd - | GrafiteAst.Macro (_, mac) -> - command_error (sprintf "The macro %s can't be in a script" - (GrafiteAstPp.pp_macro_ast mac)) - -let eval_comment status c = status - - -let eval_ast - ?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st -= - let opts = { - do_heavy_checks = do_heavy_checks ; - include_paths = include_paths; - clean_baseuri = clean_baseuri } - in - match st with - | GrafiteAst.Executable (_,ex) -> eval_executable opts status ex - | GrafiteAst.Comment (_,c) -> eval_comment status c - -let eval_from_stream - ?do_heavy_checks ?include_paths ?clean_baseuri status str cb -= - try - while true do - let ast = GrafiteParser.parse_statement str in - cb !status ast; - status := eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast - done - with End_of_file -> () + if b then + lexicon_status,acc + else + let new_lexicon_status = + LexiconEngine.set_proof_aliases lexicon_status [k,value] + in + new_lexicon_status, + ((new_grafite_status,new_lexicon_status),Some (k,value))::acc + ) (lexicon_status,[]) new_aliases + in + ((new_grafite_status,new_lexicon_status),None)::intermediate_states -(* to avoid a long list of recursive functions *) -let _ = eval_from_stream_ref := eval_from_stream - -let eval_from_stream_greedy - ?do_heavy_checks ?include_paths ?clean_baseuri status str cb +let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false) + ?do_heavy_checks ?clean_baseuri lexicon_status grafite_status str cb = - while true do - print_string "matita> "; - flush stdout; - let ast = GrafiteParser.parse_statement str in - cb !status ast; - status := eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast - done + let rec loop lexicon_status grafite_status statuses = + let loop = + if first_statement_only then + fun _ _ _ -> raise End_of_file + else + loop + in + if prompt then (print_string "matita> "; flush stdout); + try + let lexicon_status,ast = + GrafiteParser.parse_statement ~include_paths str lexicon_status + in + (match ast with + GrafiteParser.LNone _ -> + loop lexicon_status grafite_status + (((grafite_status,lexicon_status),None)::statuses) + | GrafiteParser.LSome ast -> + cb grafite_status ast; + let new_statuses = + eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status + grafite_status ast in + let grafite_status,lexicon_status = + match new_statuses with + [] -> assert false + | (s,_)::_ -> s + in + loop lexicon_status grafite_status (new_statuses @ statuses)) + with + End_of_file -> statuses + in + loop lexicon_status grafite_status [] ;; -let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str = - eval_from_stream - ?do_heavy_checks ?include_paths ?clean_baseuri status (Stream.of_string str) (fun _ _ ->()) - -let default_options () = -(* - let options = - StringMap.add "baseuri" - (String - (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner")) - no_options - in -*) - let options = - StringMap.add "basedir" - (String (Helm_registry.get "matita.basedir")) - no_options - in - options - -let initial_status = - lazy { - aliases = DisambiguateTypes.empty_environment; - moo_content_rev = []; - proof_status = No_proof; - options = default_options (); - objects = []; - notation_ids = []; - } - +let eval_string ~first_statement_only ~include_paths ?do_heavy_checks + ?clean_baseuri lexicon_status status str += + eval_from_stream ~first_statement_only ~include_paths ?do_heavy_checks + ?clean_baseuri lexicon_status status (Ulexing.from_utf8_string str) + (fun _ _ -> ())