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