helm/matita/matitaEngine.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 open Printf
  27 open MatitaTypes
  28
  29 exception Drop;;
  30 exception UnableToInclude of string;;
  31
  32 let debug = false ;;
  33 let debug_print = if debug then prerr_endline else ignore ;;
  34
  35 type options = { do_heavy_checks: bool ; include_paths: string list }
  36
  37 type statement =
  38   (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement
  39
  40 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
  41   * names as long as they are available, then it fallbacks to name generation
  42   * using FreshNamesGenerator module *)
  43 let namer_of names =
  44   let len = List.length names in
  45   let count = ref 0 in
  46   fun metasenv context name ~typ ->
  47     if !count < len then begin
  48       let name = Cic.Name (List.nth names !count) in
  49       incr count;
  50       name
  51     end else
  52       FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
  53
  54 let tactic_of_ast = function
  55   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
  56   | GrafiteAst.Apply (_, term) -> Tactics.apply term
  57   | GrafiteAst.Assumption _ -> Tactics.assumption
  58   | GrafiteAst.Auto (_,depth,width) ->
  59       AutoTactic.auto_tac ?depth ?width ~dbd:(MatitaDb.instance ()) ()
  60   | GrafiteAst.Change (_, pattern, with_what) ->
  61      Tactics.change ~pattern with_what
  62   | GrafiteAst.Clear (_,id) -> Tactics.clear id
  63   | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
  64   | GrafiteAst.Contradiction _ -> Tactics.contradiction
  65   | GrafiteAst.Compare (_, term) -> Tactics.compare term
  66   | GrafiteAst.Constructor (_, n) -> Tactics.constructor n
  67   | GrafiteAst.Cut (_, ident, term) ->
  68      let names = match ident with None -> [] | Some id -> [id] in
  69      Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
  70   | GrafiteAst.DecideEquality _ -> Tactics.decide_equality
  71   | GrafiteAst.Decompose (_,term) -> Tactics.decompose term
  72   | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
  73   | GrafiteAst.Elim (_, what, using, depth, names) ->
  74       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) what
  75   | GrafiteAst.ElimType (_, what, using, depth, names) ->
  76       Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) what
  77   | GrafiteAst.Exact (_, term) -> Tactics.exact term
  78   | GrafiteAst.Exists _ -> Tactics.exists
  79   | GrafiteAst.Fail _ -> Tactics.fail
  80   | GrafiteAst.Fold (_, reduction_kind, term, pattern) ->
  81      let reduction =
  82       match reduction_kind with
  83        | `Normalize -> CicReduction.normalize ~delta:false ~subst:[]
  84        | `Reduce -> ProofEngineReduction.reduce
  85        | `Simpl -> ProofEngineReduction.simpl
  86        | `Whd -> CicReduction.whd ~delta:false ~subst:[]
  87      in
  88       Tactics.fold ~reduction ~term ~pattern
  89   | GrafiteAst.Fourier _ -> Tactics.fourier
  90   | GrafiteAst.FwdSimpl (_, hyp, names) ->
  91      Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~dbd:(MatitaDb.instance ()) hyp
  92   | GrafiteAst.Generalize (_,pattern,ident) ->
  93      let names = match ident with None -> [] | Some id -> [id] in
  94      Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern
  95   | GrafiteAst.Goal (_, n) -> Tactics.set_goal n
  96   | GrafiteAst.IdTac _ -> Tactics.id
  97   | GrafiteAst.Injection (_,term) -> Tactics.injection term
  98   | GrafiteAst.Intros (_, None, names) ->
  99       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
 100   | GrafiteAst.Intros (_, Some num, names) ->
 101       PrimitiveTactics.intros_tac ~howmany:num
 102         ~mk_fresh_name_callback:(namer_of names) ()
 103   | GrafiteAst.LApply (_, how_many, to_what, what, ident) ->
 104      let names = match ident with None -> [] | Some id -> [id] in
 105      Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many ~to_what what
 106   | GrafiteAst.Left _ -> Tactics.left
 107   | GrafiteAst.LetIn (loc,term,name) ->
 108       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
 109   | GrafiteAst.Reduce (_, reduction_kind, pattern) ->
 110       (match reduction_kind with
 111       | `Normalize -> Tactics.normalize ~pattern
 112       | `Reduce -> Tactics.reduce ~pattern
 113       | `Simpl -> Tactics.simpl ~pattern
 114       | `Whd -> Tactics.whd ~pattern)
 115   | GrafiteAst.Reflexivity _ -> Tactics.reflexivity
 116   | GrafiteAst.Replace (_, pattern, with_what) ->
 117      Tactics.replace ~pattern ~with_what
 118   | GrafiteAst.Rewrite (_, direction, t, pattern) ->
 119      EqualityTactics.rewrite_tac ~direction ~pattern t
 120   | GrafiteAst.Right _ -> Tactics.right
 121   | GrafiteAst.Ring _ -> Tactics.ring
 122   | GrafiteAst.Split _ -> Tactics.split
 123   | GrafiteAst.Symmetry _ -> Tactics.symmetry
 124   | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
 125
 126 let disambiguate_term status term =
 127   let (aliases, metasenv, cic, _) =
 128     match
 129       MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
 130         ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
 131         ~metasenv:(MatitaMisc.get_proof_metasenv status) term
 132     with
 133     | [x] -> x
 134     | _ -> assert false
 135   in
 136   let proof_status =
 137     match status.proof_status with
 138     | No_proof -> Intermediate metasenv
 139     | Incomplete_proof ((uri, _, proof, ty), goal) ->
 140         Incomplete_proof ((uri, metasenv, proof, ty), goal)
 141     | Intermediate _ -> Intermediate metasenv
 142     | Proof _ -> assert false
 143   in
 144   let status = { status with proof_status = proof_status } in
 145   let status = MatitaSync.set_proof_aliases status aliases in
 146   status, cic
 147
 148 let disambiguate_pattern status (wanted, hyp_paths, goal_path) =
 149   let interp path = Disambiguate.interpretate_path [] status.aliases path in
 150   let goal_path = interp goal_path in
 151   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
 152   let status,wanted =
 153    match wanted with
 154       None -> status,None
 155     | Some wanted ->
 156        let status,wanted = disambiguate_term status wanted in
 157         status, Some wanted
 158   in
 159    status, (wanted, hyp_paths ,goal_path)
 160
 161 let disambiguate_tactic status = function
 162   | GrafiteAst.Apply (loc, term) ->
 163       let status, cic = disambiguate_term status term in
 164       status, GrafiteAst.Apply (loc, cic)
 165   | GrafiteAst.Absurd (loc, term) ->
 166       let status, cic = disambiguate_term status term in
 167       status, GrafiteAst.Absurd (loc, cic)
 168   | GrafiteAst.Assumption loc -> status, GrafiteAst.Assumption loc
 169   | GrafiteAst.Auto (loc,depth,width) -> status, GrafiteAst.Auto (loc,depth,width)
 170   | GrafiteAst.Change (loc, pattern, with_what) ->
 171       let status, with_what = disambiguate_term status with_what in
 172       let status, pattern = disambiguate_pattern status pattern in
 173       status, GrafiteAst.Change (loc, pattern, with_what)
 174   | GrafiteAst.Clear (loc,id) -> status,GrafiteAst.Clear (loc,id)
 175   | GrafiteAst.ClearBody (loc,id) -> status,GrafiteAst.ClearBody (loc,id)
 176   | GrafiteAst.Compare (loc,term) ->
 177       let status, term = disambiguate_term status term in
 178       status, GrafiteAst.Compare (loc,term)
 179   | GrafiteAst.Constructor (loc,n) ->
 180       status, GrafiteAst.Constructor (loc,n)
 181   | GrafiteAst.Contradiction loc ->
 182       status, GrafiteAst.Contradiction loc
 183   | GrafiteAst.Cut (loc, ident, term) ->
 184       let status, cic = disambiguate_term status term in
 185       status, GrafiteAst.Cut (loc, ident, cic)
 186   | GrafiteAst.DecideEquality loc ->
 187       status, GrafiteAst.DecideEquality loc
 188   | GrafiteAst.Decompose (loc,term) ->
 189       let status,term = disambiguate_term status term in
 190       status, GrafiteAst.Decompose(loc,term)
 191   | GrafiteAst.Discriminate (loc,term) ->
 192       let status,term = disambiguate_term status term in
 193       status, GrafiteAst.Discriminate(loc,term)
 194   | GrafiteAst.Exact (loc, term) ->
 195       let status, cic = disambiguate_term status term in
 196       status, GrafiteAst.Exact (loc, cic)
 197   | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
 198       let status, what = disambiguate_term status what in
 199       let status, using = disambiguate_term status using in
 200       status, GrafiteAst.Elim (loc, what, Some using, depth, idents)
 201   | GrafiteAst.Elim (loc, what, None, depth, idents) ->
 202       let status, what = disambiguate_term status what in
 203       status, GrafiteAst.Elim (loc, what, None, depth, idents)
 204   | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
 205       let status, what = disambiguate_term status what in
 206       let status, using = disambiguate_term status using in
 207       status, GrafiteAst.ElimType (loc, what, Some using, depth, idents)
 208   | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
 209       let status, what = disambiguate_term status what in
 210       status, GrafiteAst.ElimType (loc, what, None, depth, idents)
 211   | GrafiteAst.Exists loc -> status, GrafiteAst.Exists loc
 212   | GrafiteAst.Fail loc -> status,GrafiteAst.Fail loc
 213   | GrafiteAst.Fold (loc,reduction_kind, term, pattern) ->
 214      let status, pattern = disambiguate_pattern status pattern in
 215      let status, term = disambiguate_term status term in
 216      status, GrafiteAst.Fold (loc,reduction_kind, term, pattern)
 217   | GrafiteAst.FwdSimpl (loc, hyp, names) ->
 218      status, GrafiteAst.FwdSimpl (loc, hyp, names)
 219   | GrafiteAst.Fourier loc -> status, GrafiteAst.Fourier loc
 220   | GrafiteAst.Generalize (loc,pattern,ident) ->
 221       let status, pattern = disambiguate_pattern status pattern in
 222       status, GrafiteAst.Generalize(loc,pattern,ident)
 223   | GrafiteAst.Goal (loc, g) -> status, GrafiteAst.Goal (loc, g)
 224   | GrafiteAst.IdTac loc -> status,GrafiteAst.IdTac loc
 225   | GrafiteAst.Injection (loc,term) ->
 226       let status, term = disambiguate_term status term in
 227       status, GrafiteAst.Injection (loc,term)
 228   | GrafiteAst.Intros (loc, num, names) ->
 229       status, GrafiteAst.Intros (loc, num, names)
 230   | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
 231      let f term (status, to_what) =
 232         let status, term = disambiguate_term status term in
 233         status, term :: to_what
 234      in
 235      let status, to_what = List.fold_right f to_what (status, []) in
 236      let status, what = disambiguate_term status what in
 237      status, GrafiteAst.LApply (loc, depth, to_what, what, ident)
 238   | GrafiteAst.Left loc -> status, GrafiteAst.Left loc
 239   | GrafiteAst.LetIn (loc, term, name) ->
 240       let status, term = disambiguate_term status term in
 241       status, GrafiteAst.LetIn (loc,term,name)
 242   | GrafiteAst.Reduce (loc, reduction_kind, pattern) ->
 243       let status, pattern = disambiguate_pattern status pattern in
 244       status, GrafiteAst.Reduce(loc, reduction_kind, pattern)
 245   | GrafiteAst.Reflexivity loc -> status, GrafiteAst.Reflexivity loc
 246   | GrafiteAst.Replace (loc, pattern, with_what) ->
 247       let status, pattern = disambiguate_pattern status pattern in
 248       let status, with_what = disambiguate_term status with_what in
 249       status, GrafiteAst.Replace (loc, pattern, with_what)
 250   | GrafiteAst.Rewrite (loc, dir, t, pattern) ->
 251       let status, term = disambiguate_term status t in
 252       let status, pattern = disambiguate_pattern status pattern in
 253       status, GrafiteAst.Rewrite (loc, dir, term, pattern)
 254   | GrafiteAst.Right loc -> status, GrafiteAst.Right loc
 255   | GrafiteAst.Ring loc -> status, GrafiteAst.Ring loc
 256   | GrafiteAst.Split loc -> status, GrafiteAst.Split loc
 257   | GrafiteAst.Symmetry loc -> status, GrafiteAst.Symmetry loc
 258   | GrafiteAst.Transitivity (loc, term) ->
 259       let status, cic = disambiguate_term status term in
 260       status, GrafiteAst.Transitivity (loc, cic)
 261
 262 let apply_tactic tactic status =
 263  let status,tactic = disambiguate_tactic status tactic in
 264  let tactic = tactic_of_ast tactic in
 265  let (proof, goals) =
 266   ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status) in
 267  let dummy = -1 in
 268   { status with
 269      proof_status = MatitaTypes.Incomplete_proof (proof,dummy) }, goals
 270
 271 module MatitaStatus =
 272  struct
 273   type input_status = MatitaTypes.status
 274   type output_status = MatitaTypes.status * ProofEngineTypes.goal list
 275   type tactic = input_status -> output_status
 276
 277   let focus (status,_) goal =
 278    let proof,_ = MatitaMisc.get_proof_status status in
 279     {status with proof_status = MatitaTypes.Incomplete_proof (proof,goal)}
 280
 281   let goals (_,goals) = goals
 282
 283   let set_goals (status,_) goals = status,goals
 284
 285   let id_tac status =
 286     apply_tactic (GrafiteAst.IdTac Disambiguate.dummy_floc) status
 287
 288   let mk_tactic tac = tac
 289
 290   let apply_tactic tac = tac
 291
 292  end
 293
 294 module MatitaTacticals = Tacticals.Make(MatitaStatus)
 295
 296 let eval_tactical status tac =
 297  let rec tactical_of_ast tac =
 298   match tac with
 299     | GrafiteAst.Tactic (loc, tactic) -> apply_tactic tactic
 300     | GrafiteAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
 301        MatitaTacticals.seq ~tactics:(List.map tactical_of_ast tacticals)
 302     | GrafiteAst.Do (loc, num, tactical) ->
 303         MatitaTacticals.do_tactic ~n:num ~tactic:(tactical_of_ast tactical)
 304     | GrafiteAst.Repeat (loc, tactical) ->
 305         MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast tactical)
 306     | GrafiteAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
 307         MatitaTacticals.thens ~start:(tactical_of_ast tactical)
 308           ~continuations:(List.map tactical_of_ast tacticals)
 309     | GrafiteAst.First (loc, tacticals) ->
 310         MatitaTacticals.first
 311           ~tactics:(List.map (fun t -> "", tactical_of_ast t) tacticals)
 312     | GrafiteAst.Try (loc, tactical) ->
 313         MatitaTacticals.try_tactic ~tactic:(tactical_of_ast tactical)
 314     | GrafiteAst.Solve (loc, tacticals) ->
 315         MatitaTacticals.solve_tactics
 316          ~tactics:(List.map (fun t -> "",tactical_of_ast t) tacticals)
 317  in
 318   let status,goals = tactical_of_ast tac status in
 319   let proof,_ = MatitaMisc.get_proof_status status in
 320   let new_status =
 321    match goals with
 322    | [] ->
 323        let (_,metasenv,_,_) = proof in
 324        (match metasenv with
 325        | [] -> Proof proof
 326        | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
 327    | ng::_ -> Incomplete_proof (proof, ng)
 328   in
 329    { status with proof_status = new_status }
 330
 331 let eval_coercion status coercion =
 332   let coer_uri,coer_ty =
 333     match coercion with
 334     | Cic.Const (uri,_)
 335     | Cic.Var (uri,_) ->
 336         let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 337         (match o with
 338         | Cic.Constant (_,_,ty,_,_)
 339         | Cic.Variable (_,_,ty,_,_) ->
 340             uri,ty
 341         | _ -> assert false)
 342     | Cic.MutConstruct (uri,t,c,_) ->
 343         let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 344         (match o with
 345         | Cic.InductiveDefinition (l,_,_,_) ->
 346             let (_,_,_,cl) = List.nth l t in
 347             let (_,cty) = List.nth cl c in
 348               uri,cty
 349         | _ -> assert false)
 350     | _ -> assert false
 351   in
 352   (* we have to get the source and the tgt type uri
 353    * in Coq syntax we have already their names, but
 354    * since we don't support Funclass and similar I think
 355    * all the coercion should be of the form
 356    * (A:?)(B:?)T1->T2
 357    * So we should be able to extract them from the coercion type
 358    *)
 359   let extract_last_two_p ty =
 360     let rec aux = function
 361       | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2))
 362       | Cic.Prod( _, src, tgt) -> src, tgt
 363       | _ -> assert false
 364     in
 365     aux ty
 366   in
 367   let ty_src,ty_tgt = extract_last_two_p coer_ty in
 368   let context = [] in
 369   let src_uri =
 370     let ty_src = CicReduction.whd context ty_src in
 371      CicUtil.uri_of_term ty_src
 372   in
 373   let tgt_uri =
 374     let ty_tgt = CicReduction.whd context ty_tgt in
 375      CicUtil.uri_of_term ty_tgt
 376   in
 377   let new_coercions =
 378     (* also adds them to the Db *)
 379     CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in
 380   let status =
 381    List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status)
 382     status new_coercions in
 383   let statement_of name =
 384     GrafiteAstPp.pp_statement
 385       (GrafiteAst.Executable (Disambiguate.dummy_floc,
 386         (GrafiteAst.Command (Disambiguate.dummy_floc,
 387           (GrafiteAst.Coercion (Disambiguate.dummy_floc,
 388             (CicNotationPt.Ident (name, None)))))))) ^ "\n"
 389   in
 390   let moo_content_rev =
 391     [statement_of (UriManager.name_of_uri coer_uri)] @
 392     (List.map
 393       (fun (uri, _, _) ->
 394         statement_of (UriManager.name_of_uri uri))
 395     new_coercions) @ status.moo_content_rev
 396   in
 397   let status =  {status with moo_content_rev = moo_content_rev} in
 398   {status with proof_status = No_proof}
 399
 400 let generate_elimination_principles uri status =
 401  let elim sort status =
 402    try
 403     let uri,obj = CicElim.elim_of ~sort uri 0 in
 404      MatitaSync.add_obj uri obj status
 405    with CicElim.Can_t_eliminate -> status
 406  in
 407  List.fold_left (fun status sort -> elim sort status) status
 408   [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]
 409
 410 let generate_projections uri fields status =
 411  let projections = CicRecord.projections_of uri fields in
 412   List.fold_left
 413    (fun status (uri, name, bo) ->
 414      try
 415       let ty, ugraph =
 416         CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
 417       let bo = Unshare.unshare bo in
 418       let ty = Unshare.unshare ty in
 419       let attrs = [`Class `Projection; `Generated] in
 420       let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
 421        MatitaSync.add_obj uri obj status
 422      with
 423         CicTypeChecker.TypeCheckerFailure s ->
 424          MatitaLog.message
 425           ("Unable to create projection " ^ name ^ " cause: " ^ s);
 426          status
 427       | CicEnvironment.Object_not_found uri ->
 428          let depend = UriManager.name_of_uri uri in
 429           MatitaLog.message
 430            ("Unable to create projection " ^ name ^ " because it requires " ^ depend);
 431          status
 432   ) status projections
 433
 434 (* to avoid a long list of recursive functions *)
 435 let eval_from_stream_ref = ref (fun _ _ _ -> assert false);;
 436
 437 let disambiguate_obj status obj =
 438   let uri =
 439    match obj with
 440       GrafiteAst.Inductive (_,(name,_,_,_)::_)
 441     | GrafiteAst.Record (_,name,_,_) ->
 442        Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
 443     | GrafiteAst.Inductive _ -> assert false
 444     | GrafiteAst.Theorem _ -> None in
 445   let (aliases, metasenv, cic, _) =
 446     match
 447       MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
 448         ~aliases:(status.aliases) ~uri obj
 449     with
 450     | [x] -> x
 451     | _ -> assert false
 452   in
 453   let proof_status =
 454     match status.proof_status with
 455     | No_proof -> Intermediate metasenv
 456     | Incomplete_proof _
 457     | Intermediate _
 458     | Proof _ -> assert false
 459   in
 460   let status = { status with proof_status = proof_status } in
 461   let status = MatitaSync.set_proof_aliases status aliases in
 462   status, cic
 463
 464 let disambiguate_command status = function
 465   | GrafiteAst.Alias _
 466   | GrafiteAst.Default _
 467   | GrafiteAst.Drop _
 468   | GrafiteAst.Dump _
 469   | GrafiteAst.Include _
 470   | GrafiteAst.Interpretation _
 471   | GrafiteAst.Notation _
 472   | GrafiteAst.Qed _
 473   | GrafiteAst.Render _
 474   | GrafiteAst.Set _ as cmd ->
 475       status,cmd
 476   | GrafiteAst.Coercion (loc, term) ->
 477       let status, term = disambiguate_term status term in
 478       status, GrafiteAst.Coercion (loc,term)
 479   | GrafiteAst.Obj (loc,obj) ->
 480       let status,obj = disambiguate_obj status obj in
 481        status, GrafiteAst.Obj (loc,obj)
 482
 483 let try_open_in paths path =
 484   let rec aux = function
 485   | [] -> open_in path
 486   | p :: tl ->
 487       try
 488         open_in (p ^ "/" ^ path)
 489       with Sys_error _ -> aux tl
 490   in
 491   try
 492     aux paths
 493   with Sys_error _ as exc ->
 494     MatitaLog.error ("Unable to read " ^ path);
 495     MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths);
 496     MatitaLog.error ("current working directory is " ^ Unix.getcwd ());
 497     raise exc
 498 ;;
 499
 500 let eval_command opts status cmd =
 501   let status,cmd = disambiguate_command status cmd in
 502   let cmd,notation_ids' = CicNotation.process_notation cmd in
 503   let status =
 504     { status with notation_ids = notation_ids' @ status.notation_ids }
 505   in
 506   match cmd with
 507   | GrafiteAst.Default (loc, what, uris) as cmd ->
 508      LibraryObjects.set_default what uris;
 509      {status with moo_content_rev =
 510         (GrafiteAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
 511   | GrafiteAst.Include (loc, path) ->
 512      let path = MatitaMisc.obj_file_of_script path in
 513      let stream =
 514        try
 515          Stream.of_channel (try_open_in opts.include_paths path)
 516        with Sys_error _ -> raise (UnableToInclude path)
 517      in
 518      let status = ref status in
 519       !eval_from_stream_ref status stream (fun _ _ -> ());
 520       !status
 521   | GrafiteAst.Set (loc, name, value) ->
 522       let value =
 523         if name = "baseuri" then
 524           let v = MatitaMisc.strip_trailing_slash value in
 525           try
 526             ignore (String.index v ' ');
 527             command_error "baseuri can't contain spaces"
 528           with Not_found -> v
 529         else
 530           value
 531       in
 532       set_option status name value
 533   | GrafiteAst.Drop loc -> raise Drop
 534   | GrafiteAst.Qed loc ->
 535       let uri, metasenv, bo, ty =
 536         match status.proof_status with
 537         | Proof (Some uri, metasenv, body, ty) ->
 538             uri, metasenv, body, ty
 539         | Proof (None, metasenv, body, ty) ->
 540             command_error
 541               ("Someone allows to start a thm without giving the "^
 542                "name/uri. This should be fixed!")
 543         | _-> command_error "You can't qed an uncomplete theorem"
 544       in
 545       let suri = UriManager.string_of_uri uri in
 546       if metasenv <> [] then
 547         command_error "Proof not completed! metasenv is not empty!";
 548       let name = UriManager.name_of_uri uri in
 549       let obj = Cic.Constant (name,Some bo,ty,[],[]) in
 550       MatitaSync.add_obj uri obj status
 551   | GrafiteAst.Coercion (loc, coercion) ->
 552       eval_coercion status coercion
 553   | GrafiteAst.Alias (loc, spec) ->
 554      let aliases =
 555       match spec with
 556       | GrafiteAst.Ident_alias (id,uri) ->
 557          DisambiguateTypes.Environment.add
 558           (DisambiguateTypes.Id id)
 559           (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
 560           status.aliases
 561       | GrafiteAst.Symbol_alias (symb, instance, desc) ->
 562          DisambiguateTypes.Environment.add
 563           (DisambiguateTypes.Symbol (symb,instance))
 564           (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
 565           status.aliases
 566       | GrafiteAst.Number_alias (instance,desc) ->
 567          DisambiguateTypes.Environment.add
 568           (DisambiguateTypes.Num instance)
 569           (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases
 570      in
 571       MatitaSync.set_proof_aliases status aliases
 572   | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *)
 573   | GrafiteAst.Dump _ -> assert false   (* ZACK: to be removed *)
 574   | GrafiteAst.Interpretation _
 575   | GrafiteAst.Notation _ -> status
 576   | GrafiteAst.Obj (loc,obj) ->
 577      let ext,name =
 578       match obj with
 579          Cic.Constant (name,_,_,_,_)
 580        | Cic.CurrentProof (name,_,_,_,_,_) -> ".con",name
 581        | Cic.InductiveDefinition (types,_,_,_) ->
 582           ".ind",
 583           (match types with (name,_,_,_)::_ -> name | _ -> assert false)
 584        | _ -> assert false in
 585      let uri =
 586        UriManager.uri_of_string (MatitaMisc.qualify status name ^ ext)
 587      in
 588      let metasenv = MatitaMisc.get_proof_metasenv status in
 589      match obj with
 590      | Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
 591          let name = UriManager.name_of_uri uri in
 592          if not(CicPp.check name ty) then
 593            MatitaLog.error ("Bad name: " ^ name);
 594          if opts.do_heavy_checks then
 595            begin
 596              let dbd = MatitaDb.instance () in
 597              let similar = MetadataQuery.match_term ~dbd ty in
 598              let convertible =
 599                List.filter (
 600                  fun u ->
 601                    let t = CicUtil.term_of_uri u in
 602                    let ty',g =
 603                      CicTypeChecker.type_of_aux'
 604                        metasenv' [] t CicUniv.empty_ugraph
 605                    in
 606                    fst(CicReduction.are_convertible [] ty' ty g))
 607                similar
 608              in
 609              (match convertible with
 610              | [] -> ()
 611              | x::_ ->
 612                  MatitaLog.warn
 613                  ("Theorem already proved: " ^ UriManager.string_of_uri x ^
 614                   "\nPlease use a variant."));
 615            end;
 616          assert (metasenv = metasenv');
 617          let goalno =
 618            match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false
 619          in
 620          let initial_proof = (Some uri, metasenv, bo, ty) in
 621          { status with proof_status = Incomplete_proof (initial_proof,goalno)}
 622      | _ ->
 623          if metasenv <> [] then
 624           command_error (
 625             "metasenv not empty while giving a definition with body: " ^
 626             CicMetaSubst.ppmetasenv metasenv []);
 627          let status = MatitaSync.add_obj uri obj status in
 628           match obj with
 629              Cic.Constant _ -> status
 630            | Cic.InductiveDefinition (_,_,_,attrs) ->
 631               let status = generate_elimination_principles uri status in
 632               let rec get_record_attrs =
 633                function
 634                   [] -> None
 635                 | (`Class (`Record fields))::_ -> Some fields
 636                 | _::tl -> get_record_attrs tl
 637               in
 638                (match get_record_attrs attrs with
 639                    None -> status (* not a record *)
 640                  | Some fields -> generate_projections uri fields status)
 641            | Cic.CurrentProof _
 642            | Cic.Variable _ -> assert false
 643
 644 let eval_executable opts status ex =
 645   match ex with
 646   | GrafiteAst.Tactical (_, tac) -> eval_tactical status tac
 647   | GrafiteAst.Command (_, cmd) -> eval_command opts status cmd
 648   | GrafiteAst.Macro (_, mac) ->
 649       command_error (sprintf "The macro %s can't be in a script"
 650         (GrafiteAstPp.pp_macro_ast mac))
 651
 652 let eval_comment status c = status
 653
 654
 655 let eval_ast ?(do_heavy_checks=false) ?(include_paths=[]) status st =
 656   let opts =
 657     {do_heavy_checks = do_heavy_checks ; include_paths = include_paths}
 658   in
 659   match st with
 660   | GrafiteAst.Executable (_,ex) -> eval_executable opts status ex
 661   | GrafiteAst.Comment (_,c) -> eval_comment status c
 662
 663 let eval_from_stream ?do_heavy_checks ?include_paths status str cb =
 664   try
 665     while true do
 666       let ast = GrafiteParser.parse_statement str in
 667       cb !status ast;
 668       status := eval_ast ?do_heavy_checks ?include_paths !status ast
 669     done
 670   with End_of_file -> ()
 671
 672 (* to avoid a long list of recursive functions *)
 673 let _ = eval_from_stream_ref := eval_from_stream
 674
 675 let eval_from_stream_greedy ?do_heavy_checks ?include_paths status str cb =
 676   while true do
 677     print_string "matita> ";
 678     flush stdout;
 679     let ast = GrafiteParser.parse_statement str in
 680     cb !status ast;
 681     status := eval_ast ?do_heavy_checks ?include_paths !status ast
 682   done
 683 ;;
 684
 685 let eval_string ?do_heavy_checks ?include_paths status str =
 686   eval_from_stream
 687     ?do_heavy_checks ?include_paths status (Stream.of_string str) (fun _ _ ->())
 688
 689 let default_options () =
 690 (*
 691   let options =
 692     StringMap.add "baseuri"
 693       (String
 694         (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
 695       no_options
 696   in
 697 *)
 698   let options =
 699     StringMap.add "basedir"
 700       (String (Helm_registry.get "matita.basedir"))
 701       no_options
 702   in
 703   options
 704
 705 let initial_status =
 706   lazy {
 707     aliases = DisambiguateTypes.empty_environment;
 708     moo_content_rev = [];
 709     proof_status = No_proof;
 710     options = default_options ();
 711     objects = [];
 712     notation_ids = [];
 713   }
 714