helm/matita/matitaEngine.ml

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