helm/matita/matitaEngine.ml

   1
   2 open Printf
   3 open MatitaTypes
   4
   5 let debug = true ;;
   6 let debug_print = if debug then prerr_endline else ignore ;;
   7
   8 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
   9   * names as long as they are available, then it fallbacks to name generation
  10   * using FreshNamesGenerator module *)
  11 let namer_of names =
  12   let len = List.length names in
  13   let count = ref 0 in
  14   fun metasenv context name ~typ ->
  15     if !count < len then begin
  16       let name = Cic.Name (List.nth names !count) in
  17       incr count;
  18       name
  19     end else
  20       FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
  21
  22 let tactic_of_ast = function
  23   | TacticAst.Intros (_, None, names) ->
  24       (* TODO Zack implement intros length *)
  25       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
  26   | TacticAst.Intros (_, Some num, names) ->
  27       (* TODO Zack implement intros length *)
  28       PrimitiveTactics.intros_tac ~howmany:num
  29         ~mk_fresh_name_callback:(namer_of names) ()
  30   | TacticAst.Reflexivity _ -> Tactics.reflexivity
  31   | TacticAst.Assumption _ -> Tactics.assumption
  32   | TacticAst.Contradiction _ -> Tactics.contradiction
  33   | TacticAst.Exists _ -> Tactics.exists
  34   | TacticAst.Fourier _ -> Tactics.fourier
  35   | TacticAst.Goal (_, n) -> Tactics.set_goal n
  36   | TacticAst.Left _ -> Tactics.left
  37   | TacticAst.Right _ -> Tactics.right
  38   | TacticAst.Ring _ -> Tactics.ring
  39   | TacticAst.Split _ -> Tactics.split
  40   | TacticAst.Symmetry _ -> Tactics.symmetry
  41   | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
  42   | TacticAst.Apply (_, term) -> Tactics.apply term
  43   | TacticAst.Absurd (_, term) -> Tactics.absurd term
  44   | TacticAst.Exact (_, term) -> Tactics.exact term
  45   | TacticAst.Cut (_, term) -> Tactics.cut term
  46   | TacticAst.Elim (_, term, _) ->
  47       (* TODO Zack implement "using" argument *)
  48       (* old: Tactics.elim_intros_simpl term *)
  49       Tactics.elim_intros term
  50   | TacticAst.ElimType (_, term) -> Tactics.elim_type term
  51   | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
  52   | TacticAst.Auto (_,num) ->
  53       AutoTactic.auto_tac ~num ~dbd:(MatitaDb.instance ())
  54   | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
  55 (*
  56   (* TODO Zack a lot more of tactics to be implemented here ... *)
  57   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
  58   | TacticAst.Change of 'term * 'term * 'ident option
  59   | TacticAst.Decompose of 'ident * 'ident list
  60   | TacticAst.Discriminate of 'ident
  61   | TacticAst.Fold of reduction_kind * 'term
  62   | TacticAst.Injection of 'ident
  63   | TacticAst.Replace_pattern of 'term pattern * 'term
  64 *)
  65   | TacticAst.LetIn (loc,term,name) ->
  66       Tactics.letin ~term ~mk_fresh_name_callback:(namer_of [name])
  67   | TacticAst.ReduceAt (_,reduction_kind,ident,path) ->
  68       ProofEngineTypes.mk_tactic
  69       (fun (((_,metasenv,_,_),goal) as status) ->
  70          let metano,context,ty = CicUtil.lookup_meta goal metasenv in
  71          let where, also_in_hypotheses =
  72            if ident = "goal" then
  73              ty, false
  74            else
  75              let hyp =
  76                try
  77                  List.find (function
  78                    | Some (Cic.Name name,entry) when name = ident -> true
  79                    | _ -> false)
  80                  context
  81                with
  82                  Not_found -> raise (ProofEngineTypes.Fail (ident ^ " is not an hypothesis"))
  83              in
  84              (match hyp with
  85              | Some (_, Cic.Decl term) -> term
  86              | Some (_, Cic.Def (term,ty)) -> term
  87              | None -> assert false),true
  88          in
  89          let pointers = CicUtil.select ~term:where ~context:path in
  90           (match reduction_kind with
  91           | `Normalize ->
  92               ProofEngineTypes.apply_tactic
  93                 (Tactics.normalize ~also_in_hypotheses ~terms:(Some pointers))
  94                 status
  95           | `Reduce ->
  96               ProofEngineTypes.apply_tactic
  97                 (Tactics.reduce ~also_in_hypotheses ~terms:(Some pointers))
  98                 status
  99           | `Simpl ->
 100               ProofEngineTypes.apply_tactic
 101                 (Tactics.simpl ~also_in_hypotheses ~terms:(Some pointers))
 102                 status
 103           | `Whd ->
 104               ProofEngineTypes.apply_tactic
 105                 (Tactics.whd ~also_in_hypotheses ~terms:(Some pointers))
 106                 status))
 107   | TacticAst.Reduce (_,reduction_kind,opts) ->
 108       let terms, also_in_hypotheses =
 109         match opts with
 110         | Some (l,`Goal) -> Some l, false
 111         | Some (l,`Everywhere) -> Some l, true
 112         | None -> None, false
 113       in
 114       (match reduction_kind with
 115       | `Normalize -> Tactics.normalize ~also_in_hypotheses ~terms
 116       | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms
 117       | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms
 118       | `Whd -> Tactics.whd ~also_in_hypotheses ~terms)
 119   | TacticAst.Rewrite (_,dir,t,ident) ->
 120       if dir = `Left then
 121         EqualityTactics.rewrite_tac ~term:t
 122       else
 123         EqualityTactics.rewrite_back_tac ~term:t
 124   | _ -> assert false
 125
 126 let eval_tactical status tac =
 127   let apply_tactic tactic =
 128     let (proof, goals) =
 129       ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
 130     in
 131     let new_status =
 132       match goals with
 133       | [] ->
 134           let (_,metasenv,_,_) = proof in
 135           (match metasenv with
 136           | [] -> Proof proof
 137           | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
 138       | ng::_ -> Incomplete_proof (proof, ng)
 139     in
 140     { status with proof_status = new_status }
 141   in
 142   let rec tactical_of_ast = function
 143     | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
 144     | TacticAst.Fail loc -> Tacticals.fail
 145     | TacticAst.Do (loc, num, tactical) ->
 146         Tacticals.do_tactic num (tactical_of_ast tactical)
 147     | TacticAst.IdTac loc -> Tacticals.id_tac
 148     | TacticAst.Repeat (loc, tactical) ->
 149         Tacticals.repeat_tactic (tactical_of_ast tactical)
 150     | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
 151         Tacticals.seq (List.map tactical_of_ast tacticals)
 152     | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
 153         Tacticals.thens (tactical_of_ast tactical)
 154           (List.map tactical_of_ast tacticals)
 155     | TacticAst.Tries (loc, tacticals) ->
 156         Tacticals.try_tactics
 157           (List.map (fun t -> "", tactical_of_ast t) tacticals)
 158     | TacticAst.Try (loc, tactical) ->
 159         Tacticals.try_tactic (tactical_of_ast tactical)
 160   in
 161   apply_tactic (tactical_of_ast tac)
 162
 163 (** given a uri and a type list (the contructors types) builds a list of pairs
 164  *  (name,uri) that is used to generate authomatic aliases **)
 165 let extract_alias types uri =
 166   fst(List.fold_left (
 167     fun (acc,i) (name, _, _, cl) ->
 168       ((name, UriManager.string_of_uriref (uri,[i]))
 169       ::
 170       (fst(List.fold_left (
 171         fun (acc,j) (name,_) ->
 172           (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1)
 173         ) (acc,1) cl))),i+1
 174   ) ([],0) types)
 175
 176 (** adds a (name,uri) list l to a disambiguation environment e **)
 177 let env_of_list l e =
 178   let module DT = DisambiguateTypes in
 179   let module DTE = DisambiguateTypes.Environment in
 180   List.fold_left (
 181     fun e (name,uri) ->
 182       DTE.add
 183        (DT.Id name)
 184        (uri,fun _ _ _ -> CicUtil.term_of_uri uri)
 185        e
 186   ) e l
 187
 188 let eval_coercion status coercion =
 189   let coer_uri,coer_ty =
 190     match coercion with
 191     | Cic.Const (uri,_)
 192     | Cic.Var (uri,_) ->
 193         let o,_ =
 194           CicEnvironment.get_obj CicUniv.empty_ugraph uri
 195         in
 196         (match o with
 197         | Cic.Constant (_,_,ty,_,_)
 198         | Cic.Variable (_,_,ty,_,_) ->
 199             uri,ty
 200         | _ -> assert false)
 201     | Cic.MutConstruct (uri,t,c,_) ->
 202         let o,_ =
 203           CicEnvironment.get_obj CicUniv.empty_ugraph uri
 204         in
 205         (match o with
 206         | Cic.InductiveDefinition (l,_,_,_) ->
 207             let (_,_,_,cl) = List.nth l t in
 208             let (_,cty) = List.nth cl c in
 209               uri,cty
 210         | _ -> assert false)
 211     | _ -> assert false
 212   in
 213   (* we have to get the source and the tgt type uri
 214    * in Coq syntax we have already their names, but
 215    * since we don't support Funclass and similar I think
 216    * all the coercion should be of the form
 217    * (A:?)(B:?)T1->T2
 218    * So we should be able to extract them from the coercion type
 219    *)
 220   let extract_last_two_p ty =
 221     let rec aux = function
 222       | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2))
 223       | Cic.Prod( _, src, tgt) -> src, tgt
 224       | _ -> assert false
 225     in
 226     aux ty
 227   in
 228   let ty_src,ty_tgt = extract_last_two_p coer_ty in
 229   let context = [] in
 230   let src_uri =
 231     let ty_src = CicReduction.whd context ty_src in
 232     UriManager.uri_of_string (CicUtil.uri_of_term ty_src)
 233   in
 234   let tgt_uri =
 235     let ty_tgt = CicReduction.whd context ty_tgt in
 236     UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt)
 237   in
 238   let new_coercions =
 239     (* also adds them to the Db *)
 240     CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri
 241   in
 242   let status =
 243     List.fold_left (
 244       fun s (uri,o,ugraph) ->
 245         match o with
 246         | Cic.Constant (_,Some body, ty, params, attrs) ->
 247             MatitaSync.add_constant ~uri ~body ~ty ~ugraph ~params ~attrs status
 248         | _ -> assert false
 249     ) status new_coercions
 250   in
 251   {status with proof_status = No_proof}
 252
 253 let eval_command status cmd =
 254   match cmd with
 255   | TacticAst.Set (loc, name, value) -> set_option status name value
 256   | TacticAst.Qed loc ->
 257       let uri, metasenv, bo, ty =
 258         match status.proof_status with
 259         | Proof (Some uri, metasenv, body, ty) ->
 260             uri, metasenv, body, ty
 261         | Proof (None, metasenv, body, ty) ->
 262             command_error
 263               ("Someone allows to start a thm without giving the "^
 264                "name/uri. This should be fixed!")
 265         | _-> command_error "You can't qed an uncomplete theorem"
 266       in
 267       let suri = UriManager.string_of_uri uri in
 268       if metasenv <> [] then
 269         command_error "Proof not completed! metasenv is not empty!";
 270       let proved_ty,ugraph =
 271         CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
 272       in
 273       let b,ugraph =
 274         CicReduction.are_convertible [] proved_ty ty ugraph
 275       in
 276       if not b then
 277         command_error
 278           ("The type of your proof is not convertible with the "^
 279           "type you've declared!");
 280       MatitaLog.message (sprintf "%s defined" suri);
 281       let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
 282       let status =
 283         let name = UriManager.name_of_uri uri in
 284         let new_env = env_of_list [(name,suri)] status.aliases in
 285         {status with aliases = new_env }
 286       in
 287       {status with proof_status = No_proof }
 288   | TacticAst.Inductive (loc, dummy_params, types) ->
 289       (* dummy_params are not real params, it is a list of nothing, and the only
 290        * semantic content is the len, that is leftno (note: leftno and pamaters
 291        * have nothing in common).
 292        *)
 293       let suri =
 294         match types with
 295         | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
 296         | _ -> assert false
 297       in
 298       let uri = UriManager.uri_of_string suri in
 299       let leftno = List.length dummy_params in
 300       let obj = Cic.InductiveDefinition (types, [], leftno, []) in
 301       let ugraph =
 302         CicTypeChecker.typecheck_mutual_inductive_defs uri
 303           (types, [], leftno) CicUniv.empty_ugraph
 304       in
 305       let status =
 306         MatitaSync.add_inductive_def
 307           ~uri ~types ~params:[] ~leftno ~ugraph status
 308       in
 309       (* aliases for the constructors and types *)
 310       let aliases = env_of_list (extract_alias types uri) status.aliases in
 311       (* aliases for the eliminations principles *)
 312       let aliases =
 313         let base = String.sub suri 0 (String.length suri - 4)  in
 314         env_of_list
 315         (List.fold_left (
 316           fun acc suffix ->
 317             if List.exists (
 318               fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix
 319             ) status.objects then
 320               let u = base ^ suffix in
 321               (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc
 322             else
 323               acc
 324         ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases
 325       in
 326       let status = {status with proof_status = No_proof } in
 327       { status with aliases = aliases}
 328   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
 329       let uri =
 330         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
 331       in
 332       let goalno = 1 in
 333       let metasenv, body =
 334         match status.proof_status with
 335         | Intermediate metasenv ->
 336             ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
 337         | _-> assert false
 338       in
 339       let initial_proof = (Some uri, metasenv, body, ty) in
 340       { status with proof_status = Incomplete_proof (initial_proof,goalno)}
 341   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
 342       let uri =
 343         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
 344       in
 345       let metasenv = MatitaMisc.get_proof_metasenv status in
 346       let (body_type, ugraph) =
 347         CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
 348       in
 349       let (subst, metasenv, ugraph) =
 350         CicUnification.fo_unif metasenv [] body_type ty ugraph
 351       in
 352       if metasenv <> [] then
 353         command_error (
 354           "metasenv not empty while giving a definition with body: " ^
 355           CicMetaSubst.ppmetasenv metasenv []) ;
 356       let body = CicMetaSubst.apply_subst subst body in
 357       let ty = CicMetaSubst.apply_subst subst ty in
 358       let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
 359       let status =
 360         let suri = UriManager.string_of_uri uri in
 361         let new_env = env_of_list [(name,suri)] status.aliases in
 362         {status with aliases = new_env }
 363       in
 364       {status with proof_status = No_proof}
 365   | TacticAst.Theorem (_, _, None, _, _) ->
 366       command_error "The grammar should avoid having unnamed theorems!"
 367   | TacticAst.Coercion (loc, coercion) ->
 368       eval_coercion status coercion
 369   | TacticAst.Alias (loc, spec) ->
 370       match spec with
 371       | TacticAst.Ident_alias (id,uri) ->
 372           {status with aliases =
 373             DisambiguateTypes.Environment.add
 374               (DisambiguateTypes.Id id)
 375               ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
 376               status.aliases }
 377       | TacticAst.Symbol_alias (symb, instance, desc) ->
 378           {status with aliases =
 379             DisambiguateTypes.Environment.add
 380               (DisambiguateTypes.Symbol (symb,instance))
 381               (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
 382               status.aliases }
 383       | TacticAst.Number_alias (instance,desc) ->
 384           {status with aliases =
 385             DisambiguateTypes.Environment.add
 386               (DisambiguateTypes.Num instance)
 387               (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
 388
 389 let eval_executable status ex =
 390   match ex with
 391   | TacticAst.Tactical (_, tac) -> eval_tactical status tac
 392   | TacticAst.Command (_, cmd) -> eval_command status cmd
 393   | TacticAst.Macro (_, mac) ->
 394       command_error (sprintf "The macro %s can't be in a script"
 395         (TacticAstPp.pp_macro_cic mac))
 396
 397 let eval_comment status c = status
 398
 399 let eval status st =
 400   match st with
 401   | TacticAst.Executable (_,ex) -> eval_executable status ex
 402   | TacticAst.Comment (_,c) -> eval_comment status c
 403
 404 let disambiguate_term status term =
 405   let (aliases, metasenv, cic, _) =
 406     match
 407       MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
 408         ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
 409         ~metasenv:(MatitaMisc.get_proof_metasenv status) term
 410     with
 411     | [x] -> x
 412     | _ -> assert false
 413   in
 414   let proof_status =
 415     match status.proof_status with
 416     | No_proof -> Intermediate metasenv
 417     | Incomplete_proof ((uri, _, proof, ty), goal) ->
 418         Incomplete_proof ((uri, metasenv, proof, ty), goal)
 419     | Intermediate _ -> Intermediate metasenv
 420     | Proof _ -> assert false
 421   in
 422   let status =
 423     { status with
 424         aliases = aliases;
 425         proof_status = proof_status }
 426   in
 427   status, cic
 428
 429 let disambiguate_terms status terms =
 430   let term = CicAst.pack terms in
 431   let status, term = disambiguate_term status term in
 432   status, CicUtil.unpack term
 433
 434 let disambiguate_tactic status = function
 435   | TacticAst.Transitivity (loc, term) ->
 436       let status, cic = disambiguate_term status term in
 437       status, TacticAst.Transitivity (loc, cic)
 438   | TacticAst.Apply (loc, term) ->
 439       let status, cic = disambiguate_term status term in
 440       status, TacticAst.Apply (loc, cic)
 441   | TacticAst.Absurd (loc, term) ->
 442       let status, cic = disambiguate_term status term in
 443       status, TacticAst.Absurd (loc, cic)
 444   | TacticAst.Exact (loc, term) ->
 445       let status, cic = disambiguate_term status term in
 446       status, TacticAst.Exact (loc, cic)
 447   | TacticAst.Cut (loc, term) ->
 448       let status, cic = disambiguate_term status term in
 449       status, TacticAst.Cut (loc, cic)
 450   | TacticAst.Elim (loc, term, Some term') ->
 451       let status, cic1 = disambiguate_term status term in
 452       let status, cic2 = disambiguate_term status term' in
 453       status, TacticAst.Elim (loc, cic1, Some cic2)
 454   | TacticAst.Elim (loc, term, None) ->
 455       let status, cic = disambiguate_term status term in
 456       status, TacticAst.Elim (loc, cic, None)
 457   | TacticAst.ElimType (loc, term) ->
 458       let status, cic = disambiguate_term status term in
 459       status, TacticAst.ElimType (loc, cic)
 460   | TacticAst.Replace (loc, what, with_what) ->
 461       let status, cic1 = disambiguate_term status what in
 462       let status, cic2 = disambiguate_term status with_what in
 463       status, TacticAst.Replace (loc, cic1, cic2)
 464   | TacticAst.Change (loc, what, with_what, ident) ->
 465       let status, cic1 = disambiguate_term status what in
 466       let status, cic2 = disambiguate_term status with_what in
 467       status, TacticAst.Change (loc, cic1, cic2, ident)
 468 (*
 469   (* TODO Zack a lot more of tactics to be implemented here ... *)
 470   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
 471   | TacticAst.Change of 'term * 'term * 'ident option
 472   | TacticAst.Decompose of 'ident * 'ident list
 473   | TacticAst.Discriminate of 'ident
 474   | TacticAst.Fold of reduction_kind * 'term
 475   | TacticAst.Injection of 'ident
 476   | TacticAst.Replace_pattern of 'term pattern * 'term
 477 *)
 478   | TacticAst.LetIn (loc,term,name) ->
 479       let status, term = disambiguate_term status term in
 480       status, TacticAst.LetIn (loc,term,name)
 481   | TacticAst.ReduceAt (loc, reduction_kind, ident, path) ->
 482       let path = Disambiguate.interpretate [] status.aliases path in
 483       status, TacticAst.ReduceAt(loc, reduction_kind, ident, path)
 484   | TacticAst.Reduce (loc, reduction_kind, opts) ->
 485       let status, opts =
 486         match opts with
 487         | None -> status, None
 488         | Some (l,pat) ->
 489             let status, l =
 490               List.fold_right (fun t (status,acc) ->
 491                 let status',t' = disambiguate_term status t in
 492                 status', t'::acc)
 493               l (status,[])
 494             in
 495             status, Some (l, pat)
 496       in
 497       status, TacticAst.Reduce (loc, reduction_kind, opts)
 498   | TacticAst.Rewrite (loc,dir,t,ident) ->
 499       let status, term = disambiguate_term status t in
 500       status, TacticAst.Rewrite (loc,dir,term,ident)
 501   | TacticAst.Intros (loc, num, names) ->
 502       status, TacticAst.Intros (loc, num, names)
 503   | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
 504   | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
 505   | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
 506   | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
 507   | TacticAst.Exists loc -> status, TacticAst.Exists loc
 508   | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
 509   | TacticAst.Left loc -> status, TacticAst.Left loc
 510   | TacticAst.Right loc -> status, TacticAst.Right loc
 511   | TacticAst.Ring loc -> status, TacticAst.Ring loc
 512   | TacticAst.Split loc -> status, TacticAst.Split loc
 513   | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
 514   | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
 515   | x ->
 516       print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
 517       assert false
 518
 519 let rec disambiguate_tactical status = function
 520   | TacticAst.Tactic (loc, tactic) ->
 521       let status, tac = disambiguate_tactic status tactic in
 522       status, TacticAst.Tactic (loc, tac)
 523   | TacticAst.Do (loc, num, tactical) ->
 524       let status, tac = disambiguate_tactical status tactical in
 525       status, TacticAst.Do (loc, num, tac)
 526   | TacticAst.Repeat (loc, tactical) ->
 527       let status, tac = disambiguate_tactical status tactical in
 528       status, TacticAst.Repeat (loc, tac)
 529   | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
 530       let status, tacticals = disambiguate_tacticals status tacticals in
 531       let tacticals = List.rev tacticals in
 532       status, TacticAst.Seq (loc, tacticals)
 533   | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
 534       let status, tactical = disambiguate_tactical status tactical in
 535       let status, tacticals = disambiguate_tacticals status tacticals in
 536       status, TacticAst.Then (loc, tactical, tacticals)
 537   | TacticAst.Tries (loc, tacticals) ->
 538       let status, tacticals = disambiguate_tacticals status tacticals in
 539       status, TacticAst.Tries (loc, tacticals)
 540   | TacticAst.Try (loc, tactical) ->
 541       let status, tactical = disambiguate_tactical status tactical in
 542       status, TacticAst.Try (loc, tactical)
 543   | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
 544       status, tac
 545
 546 and disambiguate_tacticals status tacticals =
 547   let status, tacticals =
 548     List.fold_left
 549       (fun (status, tacticals) tactical ->
 550         let status, tac = disambiguate_tactical status tactical in
 551         status, tac :: tacticals)
 552       (status, [])
 553       tacticals
 554   in
 555   let tacticals = List.rev tacticals in
 556   status, tacticals
 557
 558 let disambiguate_inddef status params indTypes =
 559   let add_pi binders t =
 560     List.fold_right
 561       (fun (name, ast) acc ->
 562         CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
 563       binders t
 564   in
 565   let ind_binders =
 566     List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
 567   in
 568   let binders = ind_binders @ params in
 569   let asts = ref [] in
 570   let add_ast ast = asts := ast :: !asts in
 571   let paramsno = List.length params in
 572   let indbindersno = List.length ind_binders in
 573   List.iter
 574     (fun (name, _, typ, constructors) ->
 575       add_ast (add_pi params typ);
 576       List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
 577     indTypes;
 578   let status, terms = disambiguate_terms status !asts in
 579   let terms = ref (List.rev terms) in
 580   let get_term () =
 581     match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
 582   in
 583   let uri =
 584     match indTypes with
 585     | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
 586     | _ -> assert false
 587   in
 588   let mutinds =
 589     let counter = ref 0 in
 590     List.map
 591       (fun _ ->
 592         incr counter;
 593         CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
 594       indTypes
 595   in
 596   let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
 597   let cicIndTypes =
 598     List.fold_left
 599       (fun acc (name, inductive, typ, constructors) ->
 600         let cicTyp = get_term () in
 601         let cicConstructors =
 602           List.fold_left
 603             (fun acc (name, _) ->
 604               let typ =
 605                 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
 606               in
 607               (name, typ) :: acc)
 608             [] constructors
 609         in
 610         (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
 611       [] indTypes
 612   in
 613   let cicIndTypes = List.rev cicIndTypes in
 614   status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
 615
 616 let disambiguate_command status = function
 617   | TacticAst.Inductive (loc, params, types) ->
 618       let (status, (uri, (ind_types, vars, paramsno))) =
 619         disambiguate_inddef status params types
 620       in
 621       let rec mk_list = function
 622         | 0 -> []
 623         | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
 624       in
 625       (* once we've built the cic inductive types we no longer need terms
 626          corresponding to parameters, but we need the leftno, and we encode
 627          it as the length of dummy_params
 628       *)
 629       let dummy_params = mk_list paramsno in
 630       status, TacticAst.Inductive (loc, dummy_params, ind_types)
 631   | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
 632       let status, ty = disambiguate_term status ty in
 633       let status, body =
 634         match body with
 635         | None -> status, None
 636         | Some body ->
 637             let status, body = disambiguate_term status body in
 638             status, Some body
 639       in
 640       status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
 641   | TacticAst.Coercion (loc, term) ->
 642       let status, term = disambiguate_term status term in
 643       status, TacticAst.Coercion (loc,term)
 644   | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
 645       status, cmd
 646   | TacticAst.Alias _ as x -> status, x
 647
 648 let disambiguate_executable status ex =
 649   match ex with
 650   | TacticAst.Tactical (loc, tac) ->
 651       let status, tac = disambiguate_tactical status tac in
 652       status, (TacticAst.Tactical (loc, tac))
 653   | TacticAst.Command (loc, cmd) ->
 654       let status, cmd = disambiguate_command status cmd in
 655       status, (TacticAst.Command (loc, cmd))
 656   | TacticAst.Macro (_, mac) ->
 657       command_error
 658         (sprintf ("The engine is not allowed to disambiguate any macro, "^^
 659                  "in particular %s") (TacticAstPp.pp_macro_ast mac))
 660
 661 let disambiguate_comment status c =
 662   match c with
 663   | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
 664   | TacticAst.Code (loc,ex) ->
 665         let status, ex = disambiguate_executable status ex in
 666         status, TacticAst.Code (loc,ex)
 667
 668 let disambiguate_statement status statement =
 669   match statement with
 670   | TacticAst.Comment (loc,c) ->
 671         let status, c = disambiguate_comment status c in
 672         status, TacticAst.Comment (loc,c)
 673   | TacticAst.Executable (loc,ex) ->
 674         let status, ex = disambiguate_executable status ex in
 675         status, TacticAst.Executable (loc,ex)
 676
 677 let eval_ast status ast =
 678   let status,st = disambiguate_statement status ast in
 679   (* this disambiguation step should be deferred to support tacticals *)
 680   eval status st
 681
 682 let eval_from_stream status str cb =
 683   let stl = CicTextualParser2.parse_statements str in
 684   List.fold_left
 685     (fun status ast -> cb status ast;eval_ast status ast) status
 686   stl
 687
 688 let eval_string status str =
 689   eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
 690
 691 let default_options () =
 692   let options =
 693     StringMap.add "baseuri"
 694       (String
 695         (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
 696       no_options
 697   in
 698   let options =
 699     StringMap.add "basedir"
 700       (String (Helm_registry.get "matita.basedir" ))
 701       options
 702   in
 703   options
 704
 705 let initial_status =
 706   lazy {
 707     aliases = DisambiguateTypes.empty_environment;
 708     proof_status = No_proof;
 709     options = default_options ();
 710     objects = [];
 711   }
 712