The status has been extended with a "universe", that is a

[helm.git] / components / grafite_engine / grafiteEngine.ml

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 4539029af26e1b6d276904701c2a414d81693cc7..582ad112d667e559aec395cde9a3c992731656ff 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -56,16 +56,18 @@ let namer_of names =
     end else
       FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
 
-let tactic_of_ast ast =
+let tactic_of_ast status ast =
   let module PET = ProofEngineTypes in
   match ast with
   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
   | GrafiteAst.Apply (_, term) -> Tactics.apply term
   | GrafiteAst.ApplyS (_, term, params) ->
      Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
+       ~universe:status.GrafiteTypes.universe
   | GrafiteAst.Assumption _ -> Tactics.assumption
   | GrafiteAst.Auto (_,params) ->
       AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ()) 
+       ~universe:status.GrafiteTypes.universe
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
   | GrafiteAst.Clear (_,id) -> Tactics.clear id
@@ -304,7 +306,7 @@ let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) =
  let proof = GrafiteTypes.get_current_proof status in
  let proof_status = proof, goal in
  let needs_reordering, always_opens_a_goal = classify_tactic tactic in
- let tactic = tactic_of_ast tactic in
+ let tactic = tactic_of_ast status tactic in
  (* apply tactic will change the lexicon_status ... *)
 (* prerr_endline "apply_tactic bassa"; *)
  let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in
@@ -617,6 +619,22 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
  let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
  let status,uris =
   match cmd with
+  | GrafiteAst.Index (loc,None,uri) -> 
+       assert false (* TODO: for user input *)
+  | GrafiteAst.Index (loc,Some key,uri) -> 
+      let universe = Universe.index 
+       status.GrafiteTypes.universe key (CicUtil.term_of_uri uri) in
+      let status = {status with GrafiteTypes.universe = universe} in
+(* debug
+      let msg =
+       let candidates = Universe.get_candidates status.GrafiteTypes.universe key in
+       ("candidates for " ^ (CicPp.ppterm key) ^ " = " ^ 
+         (String.concat "\n" (List.map CicPp.ppterm candidates))) 
+     in
+     prerr_endline msg;
+*)
+      let status = GrafiteTypes.add_moo_content [cmd] status in
+      status,[] 
   | GrafiteAst.Coercion (loc, uri, add_composites, arity) ->
      eval_coercion status ~add_composites uri arity
   | GrafiteAst.Default (loc, what, uris) as cmd ->
@@ -636,6 +654,20 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
            raise (IncludedFileNotCompiled (moopath_rw,baseuri))
      in
      let status = eval_from_moo.efm_go status moopath in
+(* debug
+     let lt_uri = UriManager.uri_of_string "cic:/matita/nat/orders/lt.con" in
+     let nat_uri = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in
+     let nat = Cic.MutInd(nat_uri,0,[]) in
+     let zero = Cic.MutConstruct(nat_uri,0,1,[]) in
+     let succ = Cic.MutConstruct(nat_uri,0,2,[]) in
+     let fake= Cic.Meta(-1,[]) in
+     let term= Cic.Appl [Cic.Const (lt_uri,[]);zero;Cic.Appl[succ;zero]] in     let msg =
+       let candidates = Universe.get_candidates status.GrafiteTypes.universe term in
+       ("candidates for " ^ (CicPp.ppterm term) ^ " = " ^ 
+         (String.concat "\n" (List.map CicPp.ppterm candidates))) 
+     in
+     prerr_endline msg;
+*)
      status,[]
   | GrafiteAst.Print (_,"proofterm") ->
       let _,_,p,_ = GrafiteTypes.get_current_proof status in
@@ -662,7 +694,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       let name = UriManager.name_of_uri uri in
       let obj = Cic.Constant (name,Some bo,ty,[],[]) in
       let status, lemmas = add_obj uri obj status in
-       {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
+       {status with 
+         GrafiteTypes.proof_status = GrafiteTypes.No_proof},
         uri::lemmas
   | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> 
      Setoids.add_relation id a aeq refl sym trans;