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 src_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_src) in
 230   let tgt_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) in
 231   let new_coercions =
 232     (* also adds them to the Db *)
 233     CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri
 234   in
 235   let status =
 236     List.fold_left (
 237       fun s (uri,o,ugraph) ->
 238         match o with
 239         | Cic.Constant (_,Some body, ty, params, attrs) ->
 240             MatitaSync.add_constant ~uri ~body ~ty ~ugraph ~params ~attrs status
 241         | _ -> assert false
 242     ) status new_coercions
 243   in
 244   {status with proof_status = No_proof}
 245
 246 let eval_command status cmd =
 247   match cmd with
 248   | TacticAst.Set (loc, name, value) -> set_option status name value
 249   | TacticAst.Qed loc ->
 250       let uri, metasenv, bo, ty =
 251         match status.proof_status with
 252         | Proof (Some uri, metasenv, body, ty) ->
 253             uri, metasenv, body, ty
 254         | Proof (None, metasenv, body, ty) ->
 255             command_error
 256               ("Someone allows to start a thm without giving the "^
 257                "name/uri. This should be fixed!")
 258         | _-> command_error "You can't qed an uncomplete theorem"
 259       in
 260       let suri = UriManager.string_of_uri uri in
 261       if metasenv <> [] then
 262         command_error "Proof not completed! metasenv is not empty!";
 263       let proved_ty,ugraph =
 264         CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
 265       in
 266       let b,ugraph =
 267         CicReduction.are_convertible [] proved_ty ty ugraph
 268       in
 269       if not b then
 270         command_error
 271           ("The type of your proof is not convertible with the "^
 272           "type you've declared!");
 273       MatitaLog.message (sprintf "%s defined" suri);
 274       let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
 275       let status =
 276         let name = UriManager.name_of_uri uri in
 277         let new_env = env_of_list [(name,suri)] status.aliases in
 278         {status with aliases = new_env }
 279       in
 280       {status with proof_status = No_proof }
 281   | TacticAst.Inductive (loc, dummy_params, types) ->
 282       (* dummy_params are not real params, it is a list of nothing, and the only
 283        * semantic content is the len, that is leftno (note: leftno and pamaters
 284        * have nothing in common).
 285        *)
 286       let suri =
 287         match types with
 288         | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
 289         | _ -> assert false
 290       in
 291       let uri = UriManager.uri_of_string suri in
 292       let leftno = List.length dummy_params in
 293       let obj = Cic.InductiveDefinition (types, [], leftno, []) in
 294       let ugraph =
 295         CicTypeChecker.typecheck_mutual_inductive_defs uri
 296           (types, [], leftno) CicUniv.empty_ugraph
 297       in
 298       let status =
 299         MatitaSync.add_inductive_def
 300           ~uri ~types ~params:[] ~leftno ~ugraph status
 301       in
 302       (* aliases for the constructors and types *)
 303       let aliases = env_of_list (extract_alias types uri) status.aliases in
 304       (* aliases for the eliminations principles *)
 305       let aliases =
 306         let base = String.sub suri 0 (String.length suri - 4)  in
 307         env_of_list
 308         (List.fold_left (
 309           fun acc suffix ->
 310             if List.exists (
 311               fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix
 312             ) status.objects then
 313               let u = base ^ suffix in
 314               (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc
 315             else
 316               acc
 317         ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases
 318       in
 319       let status = {status with proof_status = No_proof } in
 320       { status with aliases = aliases}
 321   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
 322       let uri =
 323         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
 324       in
 325       let goalno = 1 in
 326       let metasenv, body =
 327         match status.proof_status with
 328         | Intermediate metasenv ->
 329             ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
 330         | _-> assert false
 331       in
 332       let initial_proof = (Some uri, metasenv, body, ty) in
 333       { status with proof_status = Incomplete_proof (initial_proof,goalno)}
 334   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
 335       let uri =
 336         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
 337       in
 338       let metasenv = MatitaMisc.get_proof_metasenv status in
 339       let (body_type, ugraph) =
 340         CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
 341       in
 342       let (subst, metasenv, ugraph) =
 343         CicUnification.fo_unif metasenv [] body_type ty ugraph
 344       in
 345       if metasenv <> [] then
 346         command_error (
 347           "metasenv not empty while giving a definition with body: " ^
 348           CicMetaSubst.ppmetasenv metasenv []) ;
 349       let body = CicMetaSubst.apply_subst subst body in
 350       let ty = CicMetaSubst.apply_subst subst ty in
 351       let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
 352       let status =
 353         let suri = UriManager.string_of_uri uri in
 354         let new_env = env_of_list [(name,suri)] status.aliases in
 355         {status with aliases = new_env }
 356       in
 357       {status with proof_status = No_proof}
 358   | TacticAst.Theorem (_, _, None, _, _) ->
 359       command_error "The grammar should avoid having unnamed theorems!"
 360   | TacticAst.Coercion (loc, coercion) ->
 361       eval_coercion status coercion
 362   | TacticAst.Alias (loc, spec) ->
 363       match spec with
 364       | TacticAst.Ident_alias (id,uri) ->
 365           {status with aliases =
 366             DisambiguateTypes.Environment.add
 367               (DisambiguateTypes.Id id)
 368               ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
 369               status.aliases }
 370       | TacticAst.Symbol_alias (symb, instance, desc) ->
 371           {status with aliases =
 372             DisambiguateTypes.Environment.add
 373               (DisambiguateTypes.Symbol (symb,instance))
 374               (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
 375               status.aliases }
 376       | TacticAst.Number_alias (instance,desc) ->
 377           {status with aliases =
 378             DisambiguateTypes.Environment.add
 379               (DisambiguateTypes.Num instance)
 380               (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
 381
 382 let eval_executable status ex =
 383   match ex with
 384   | TacticAst.Tactical (_, tac) -> eval_tactical status tac
 385   | TacticAst.Command (_, cmd) -> eval_command status cmd
 386   | TacticAst.Macro (_, mac) ->
 387       command_error (sprintf "The macro %s can't be in a script"
 388         (TacticAstPp.pp_macro_cic mac))
 389
 390 let eval_comment status c = status
 391
 392 let eval status st =
 393   match st with
 394   | TacticAst.Executable (_,ex) -> eval_executable status ex
 395   | TacticAst.Comment (_,c) -> eval_comment status c
 396
 397 let disambiguate_term status term =
 398   let (aliases, metasenv, cic, _) =
 399     match
 400       MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
 401         ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
 402         ~metasenv:(MatitaMisc.get_proof_metasenv status) term
 403     with
 404     | [x] -> x
 405     | _ -> assert false
 406   in
 407   let proof_status =
 408     match status.proof_status with
 409     | No_proof -> Intermediate metasenv
 410     | Incomplete_proof ((uri, _, proof, ty), goal) ->
 411         Incomplete_proof ((uri, metasenv, proof, ty), goal)
 412     | Intermediate _ -> Intermediate metasenv
 413     | Proof _ -> assert false
 414   in
 415   let status =
 416     { status with
 417         aliases = aliases;
 418         proof_status = proof_status }
 419   in
 420   status, cic
 421
 422 let disambiguate_terms status terms =
 423   let term = CicAst.pack terms in
 424   let status, term = disambiguate_term status term in
 425   status, CicUtil.unpack term
 426
 427 let disambiguate_tactic status = function
 428   | TacticAst.Transitivity (loc, term) ->
 429       let status, cic = disambiguate_term status term in
 430       status, TacticAst.Transitivity (loc, cic)
 431   | TacticAst.Apply (loc, term) ->
 432       let status, cic = disambiguate_term status term in
 433       status, TacticAst.Apply (loc, cic)
 434   | TacticAst.Absurd (loc, term) ->
 435       let status, cic = disambiguate_term status term in
 436       status, TacticAst.Absurd (loc, cic)
 437   | TacticAst.Exact (loc, term) ->
 438       let status, cic = disambiguate_term status term in
 439       status, TacticAst.Exact (loc, cic)
 440   | TacticAst.Cut (loc, term) ->
 441       let status, cic = disambiguate_term status term in
 442       status, TacticAst.Cut (loc, cic)
 443   | TacticAst.Elim (loc, term, Some term') ->
 444       let status, cic1 = disambiguate_term status term in
 445       let status, cic2 = disambiguate_term status term' in
 446       status, TacticAst.Elim (loc, cic1, Some cic2)
 447   | TacticAst.Elim (loc, term, None) ->
 448       let status, cic = disambiguate_term status term in
 449       status, TacticAst.Elim (loc, cic, None)
 450   | TacticAst.ElimType (loc, term) ->
 451       let status, cic = disambiguate_term status term in
 452       status, TacticAst.ElimType (loc, cic)
 453   | TacticAst.Replace (loc, what, with_what) ->
 454       let status, cic1 = disambiguate_term status what in
 455       let status, cic2 = disambiguate_term status with_what in
 456       status, TacticAst.Replace (loc, cic1, cic2)
 457   | TacticAst.Change (loc, what, with_what, ident) ->
 458       let status, cic1 = disambiguate_term status what in
 459       let status, cic2 = disambiguate_term status with_what in
 460       status, TacticAst.Change (loc, cic1, cic2, ident)
 461 (*
 462   (* TODO Zack a lot more of tactics to be implemented here ... *)
 463   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
 464   | TacticAst.Change of 'term * 'term * 'ident option
 465   | TacticAst.Decompose of 'ident * 'ident list
 466   | TacticAst.Discriminate of 'ident
 467   | TacticAst.Fold of reduction_kind * 'term
 468   | TacticAst.Injection of 'ident
 469   | TacticAst.Replace_pattern of 'term pattern * 'term
 470 *)
 471   | TacticAst.LetIn (loc,term,name) ->
 472       let status, term = disambiguate_term status term in
 473       status, TacticAst.LetIn (loc,term,name)
 474   | TacticAst.ReduceAt (loc, reduction_kind, ident, path) ->
 475       let path = Disambiguate.interpretate [] status.aliases path in
 476       status, TacticAst.ReduceAt(loc, reduction_kind, ident, path)
 477   | TacticAst.Reduce (loc, reduction_kind, opts) ->
 478       let status, opts =
 479         match opts with
 480         | None -> status, None
 481         | Some (l,pat) ->
 482             let status, l =
 483               List.fold_right (fun t (status,acc) ->
 484                 let status',t' = disambiguate_term status t in
 485                 status', t'::acc)
 486               l (status,[])
 487             in
 488             status, Some (l, pat)
 489       in
 490       status, TacticAst.Reduce (loc, reduction_kind, opts)
 491   | TacticAst.Rewrite (loc,dir,t,ident) ->
 492       let status, term = disambiguate_term status t in
 493       status, TacticAst.Rewrite (loc,dir,term,ident)
 494   | TacticAst.Intros (loc, num, names) ->
 495       status, TacticAst.Intros (loc, num, names)
 496   | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
 497   | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
 498   | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
 499   | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
 500   | TacticAst.Exists loc -> status, TacticAst.Exists loc
 501   | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
 502   | TacticAst.Left loc -> status, TacticAst.Left loc
 503   | TacticAst.Right loc -> status, TacticAst.Right loc
 504   | TacticAst.Ring loc -> status, TacticAst.Ring loc
 505   | TacticAst.Split loc -> status, TacticAst.Split loc
 506   | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
 507   | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
 508   | x ->
 509       print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
 510       assert false
 511
 512 let rec disambiguate_tactical status = function
 513   | TacticAst.Tactic (loc, tactic) ->
 514       let status, tac = disambiguate_tactic status tactic in
 515       status, TacticAst.Tactic (loc, tac)
 516   | TacticAst.Do (loc, num, tactical) ->
 517       let status, tac = disambiguate_tactical status tactical in
 518       status, TacticAst.Do (loc, num, tac)
 519   | TacticAst.Repeat (loc, tactical) ->
 520       let status, tac = disambiguate_tactical status tactical in
 521       status, TacticAst.Repeat (loc, tac)
 522   | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
 523       let status, tacticals = disambiguate_tacticals status tacticals in
 524       let tacticals = List.rev tacticals in
 525       status, TacticAst.Seq (loc, tacticals)
 526   | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
 527       let status, tactical = disambiguate_tactical status tactical in
 528       let status, tacticals = disambiguate_tacticals status tacticals in
 529       status, TacticAst.Then (loc, tactical, tacticals)
 530   | TacticAst.Tries (loc, tacticals) ->
 531       let status, tacticals = disambiguate_tacticals status tacticals in
 532       status, TacticAst.Tries (loc, tacticals)
 533   | TacticAst.Try (loc, tactical) ->
 534       let status, tactical = disambiguate_tactical status tactical in
 535       status, TacticAst.Try (loc, tactical)
 536   | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
 537       status, tac
 538
 539 and disambiguate_tacticals status tacticals =
 540   let status, tacticals =
 541     List.fold_left
 542       (fun (status, tacticals) tactical ->
 543         let status, tac = disambiguate_tactical status tactical in
 544         status, tac :: tacticals)
 545       (status, [])
 546       tacticals
 547   in
 548   let tacticals = List.rev tacticals in
 549   status, tacticals
 550
 551 let disambiguate_inddef status params indTypes =
 552   let add_pi binders t =
 553     List.fold_right
 554       (fun (name, ast) acc ->
 555         CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
 556       binders t
 557   in
 558   let ind_binders =
 559     List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
 560   in
 561   let binders = ind_binders @ params in
 562   let asts = ref [] in
 563   let add_ast ast = asts := ast :: !asts in
 564   let paramsno = List.length params in
 565   let indbindersno = List.length ind_binders in
 566   List.iter
 567     (fun (name, _, typ, constructors) ->
 568       add_ast (add_pi params typ);
 569       List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
 570     indTypes;
 571   let status, terms = disambiguate_terms status !asts in
 572   let terms = ref (List.rev terms) in
 573   let get_term () =
 574     match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
 575   in
 576   let uri =
 577     match indTypes with
 578     | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
 579     | _ -> assert false
 580   in
 581   let mutinds =
 582     let counter = ref 0 in
 583     List.map
 584       (fun _ ->
 585         incr counter;
 586         CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
 587       indTypes
 588   in
 589   let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
 590   let cicIndTypes =
 591     List.fold_left
 592       (fun acc (name, inductive, typ, constructors) ->
 593         let cicTyp = get_term () in
 594         let cicConstructors =
 595           List.fold_left
 596             (fun acc (name, _) ->
 597               let typ =
 598                 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
 599               in
 600               (name, typ) :: acc)
 601             [] constructors
 602         in
 603         (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
 604       [] indTypes
 605   in
 606   let cicIndTypes = List.rev cicIndTypes in
 607   status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
 608
 609 let disambiguate_command status = function
 610   | TacticAst.Inductive (loc, params, types) ->
 611       let (status, (uri, (ind_types, vars, paramsno))) =
 612         disambiguate_inddef status params types
 613       in
 614       let rec mk_list = function
 615         | 0 -> []
 616         | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
 617       in
 618       (* once we've built the cic inductive types we no longer need terms
 619          corresponding to parameters, but we need the leftno, and we encode
 620          it as the length of dummy_params
 621       *)
 622       let dummy_params = mk_list paramsno in
 623       status, TacticAst.Inductive (loc, dummy_params, ind_types)
 624   | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
 625       let status, ty = disambiguate_term status ty in
 626       let status, body =
 627         match body with
 628         | None -> status, None
 629         | Some body ->
 630             let status, body = disambiguate_term status body in
 631             status, Some body
 632       in
 633       status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
 634   | TacticAst.Coercion (loc, term) ->
 635       let status, term = disambiguate_term status term in
 636       status, TacticAst.Coercion (loc,term)
 637   | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
 638       status, cmd
 639   | TacticAst.Alias _ as x -> status, x
 640
 641 let disambiguate_executable status ex =
 642   match ex with
 643   | TacticAst.Tactical (loc, tac) ->
 644       let status, tac = disambiguate_tactical status tac in
 645       status, (TacticAst.Tactical (loc, tac))
 646   | TacticAst.Command (loc, cmd) ->
 647       let status, cmd = disambiguate_command status cmd in
 648       status, (TacticAst.Command (loc, cmd))
 649   | TacticAst.Macro (_, mac) ->
 650       command_error
 651         (sprintf ("The engine is not allowed to disambiguate any macro, "^^
 652                  "in particular %s") (TacticAstPp.pp_macro_ast mac))
 653
 654 let disambiguate_comment status c =
 655   match c with
 656   | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
 657   | TacticAst.Code (loc,ex) ->
 658         let status, ex = disambiguate_executable status ex in
 659         status, TacticAst.Code (loc,ex)
 660
 661 let disambiguate_statement status statement =
 662   match statement with
 663   | TacticAst.Comment (loc,c) ->
 664         let status, c = disambiguate_comment status c in
 665         status, TacticAst.Comment (loc,c)
 666   | TacticAst.Executable (loc,ex) ->
 667         let status, ex = disambiguate_executable status ex in
 668         status, TacticAst.Executable (loc,ex)
 669
 670 let eval_ast status ast =
 671   let status,st = disambiguate_statement status ast in
 672   (* this disambiguation step should be deferred to support tacticals *)
 673   eval status st
 674
 675 let eval_from_stream status str cb =
 676   let stl = CicTextualParser2.parse_statements str in
 677   List.fold_left
 678     (fun status ast -> cb status ast;eval_ast status ast) status
 679   stl
 680
 681 let eval_string status str =
 682   eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
 683
 684 let default_options () =
 685   let options =
 686     StringMap.add "baseuri"
 687       (String
 688         (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
 689       no_options
 690   in
 691   let options =
 692     StringMap.add "basedir"
 693       (String (Helm_registry.get "matita.basedir" ))
 694       options
 695   in
 696   options
 697
 698 let initial_status =
 699   lazy {
 700     aliases = DisambiguateTypes.empty_environment;
 701     proof_status = No_proof;
 702     options = default_options ();
 703     objects = [];
 704   }
 705