X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=5997297cd765b2491551e91ba726e2372119f87a;hb=4e7e01cd771c07b3605ba54d3853ac34a02cb86d;hp=50095cf1364dc03234ef9ac5f1561a46e023a27f;hpb=715a957a9f7362cb002faa488160a910b9db677e;p=helm.git

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 50095cf13..5997297cd 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -40,10 +40,13 @@ let basic_eval_unification_hint (t,n) status =
 
 let inject_unification_hint =
  let basic_eval_unification_hint (t,n) 
-   ~refresh_uri_in_universe 
-   ~refresh_uri_in_term
+   ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+   ~alias_only status
  =
-  let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
+  if not alias_only then
+   let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n) status
+  else
+   status
  in
   GrafiteTypes.Serializer.register#run "unification_hints"
    basic_eval_unification_hint
@@ -51,7 +54,7 @@ let inject_unification_hint =
 
 let eval_unification_hint status t n = 
  let metasenv,subst,status,t =
-  GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,t) in
+  GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,t) in
  assert (metasenv=[]);
  let t = NCicUntrusted.apply_subst subst [] t in
  let status = basic_eval_unification_hint (t,n) status in
@@ -70,20 +73,24 @@ let basic_index_obj l status =
     status#auto_cache l) 
 ;;     
 
-let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern) status =
+let basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern) status =
  let status =
-  Interpretations.add_interpretation status dsc (symbol, args) cic_appl_pattern
+  if not alias_only then
+   Interpretations.add_interpretation status dsc (symbol, args) cic_appl_pattern
+  else
+   status
  in
- let mode = GrafiteAst.WithPreferences (*assert false*) in (* VEDI SOTTO *)
+ let mode = GrafiteAst.WithPreferences (*assert false*) in (* MATITA 1.0 VEDI SOTTO *)
  let diff =
   [DisambiguateTypes.Symbol (symbol, 0), GrafiteAst.Symbol_alias (symbol,0,dsc)]
  in
-  LexiconEngine.set_proof_aliases status ~implicit_aliases:false mode diff
+  GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
 ;;
 
 let inject_interpretation =
  let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern)
-   ~refresh_uri_in_universe ~refresh_uri_in_term
+   ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+   ~alias_only
  =
   let rec refresh =
    function
@@ -95,28 +102,110 @@ let inject_interpretation =
     | NotationPt.ApplPattern l -> NotationPt.ApplPattern (List.map refresh l)
   in
   let cic_appl_pattern = refresh cic_appl_pattern in
-   basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern)
+   basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern)
  in
   GrafiteTypes.Serializer.register#run "interpretation"
    basic_eval_interpretation
 ;;
 
 let eval_interpretation status data= 
- let status = basic_eval_interpretation data status in
+ let status = basic_eval_interpretation ~alias_only:false data status in
  let dump = inject_interpretation data::status#dump in
   status#set_dump dump
 ;;
 
+let basic_eval_alias (mode,diff) status =
+  GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
+;;
+
+let inject_alias =
+ let basic_eval_alias (mode,diff) ~refresh_uri_in_universe ~refresh_uri_in_term
+   ~refresh_uri_in_reference ~alias_only =
+   basic_eval_alias (mode,diff)
+ in
+  GrafiteTypes.Serializer.register#run "alias" basic_eval_alias
+;;
+
+let eval_alias status data= 
+ let status = basic_eval_alias data status in
+ let dump = inject_alias data::status#dump in
+  status#set_dump dump
+;;
+
+let basic_eval_input_notation (l1,l2) status =
+  GrafiteParser.extend status l1 
+   (fun env loc ->
+     NotationPt.AttributedTerm
+      (`Loc loc,TermContentPres.instantiate_level2 env l2)) 
+;;
+
+let inject_input_notation =
+ let basic_eval_input_notation (l1,l2)
+  ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+  ~alias_only status
+ =
+   if not alias_only then
+    let l1 =
+     CicNotationParser.refresh_uri_in_checked_l1_pattern
+      ~refresh_uri_in_term ~refresh_uri_in_reference l1 in
+    let l2 = NotationUtil.refresh_uri_in_term
+      ~refresh_uri_in_term ~refresh_uri_in_reference l2
+    in
+     basic_eval_input_notation (l1,l2) status
+   else
+    status
+ in
+  GrafiteTypes.Serializer.register#run "input_notation"
+   basic_eval_input_notation
+;;
+
+let eval_input_notation status data= 
+ let status = basic_eval_input_notation data status in
+ let dump = inject_input_notation data::status#dump in
+  status#set_dump dump
+;;
+
+let basic_eval_output_notation (l1,l2) status =
+ TermContentPres.add_pretty_printer status l2 l1
+;;
+
+let inject_output_notation =
+ let basic_eval_output_notation (l1,l2)
+  ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+  ~alias_only status
+ =
+  if not alias_only then
+   let l1 =
+    CicNotationParser.refresh_uri_in_checked_l1_pattern
+     ~refresh_uri_in_term ~refresh_uri_in_reference l1 in
+   let l2 = NotationUtil.refresh_uri_in_term
+     ~refresh_uri_in_term ~refresh_uri_in_reference l2
+   in
+    basic_eval_output_notation (l1,l2) status
+  else
+   status
+ in
+  GrafiteTypes.Serializer.register#run "output_notation"
+   basic_eval_output_notation
+;;
+
+let eval_output_notation status data= 
+ let status = basic_eval_output_notation data status in
+ let dump = inject_output_notation data::status#dump in
+  status#set_dump dump
+;;
 
 let record_index_obj = 
- let aux l 
-   ~refresh_uri_in_universe 
-   ~refresh_uri_in_term
+ let aux l ~refresh_uri_in_universe 
+   ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status
  =
+  if not alias_only then
     basic_index_obj
       (List.map 
         (fun ks,v -> List.map refresh_uri_in_term ks, refresh_uri_in_term v) 
-      l)
+      l) status
+  else
+   status
  in
   GrafiteTypes.Serializer.register#run "index_obj" aux
 ;;
@@ -195,9 +284,10 @@ let index_eq uri status =
 
 let record_index_eq =
  let basic_index_eq uri
-   ~refresh_uri_in_universe 
-   ~refresh_uri_in_term 
-   = index_eq (NCicLibrary.refresh_uri uri) 
+   ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference 
+   ~alias_only status
+   = if not alias_only then index_eq (NCicLibrary.refresh_uri uri) status else
+     status
  in
   GrafiteTypes.Serializer.register#run "index_eq" basic_index_eq
 ;;
@@ -221,12 +311,15 @@ let basic_eval_add_constraint (u1,u2) status =
 
 let inject_constraint =
  let basic_eval_add_constraint (u1,u2) 
-       ~refresh_uri_in_universe 
-       ~refresh_uri_in_term
+     ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+     ~alias_only status
  =
-  let u1 = refresh_uri_in_universe u1 in 
-  let u2 = refresh_uri_in_universe u2 in 
-  basic_eval_add_constraint (u1,u2)
+  if not alias_only then
+   let u1 = refresh_uri_in_universe u1 in 
+   let u2 = refresh_uri_in_universe u2 in 
+    basic_eval_add_constraint (u1,u2) status
+  else
+   status
  in
   GrafiteTypes.Serializer.register#run "constraints" basic_eval_add_constraint 
 ;;
@@ -275,6 +368,7 @@ let eval_ng_tac tac =
   | GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t) 
 (*| GrafiteAst.NDiscriminate (_,what) -> NDestructTac.discriminate_tac ~what:(text,prefix_len,what)
   | GrafiteAst.NSubst (_,what) -> NDestructTac.subst_tac ~what:(text,prefix_len,what)*)
+  | GrafiteAst.NClear (_loc, l) -> NTactics.clear_tac l
   | GrafiteAst.NDestruct (_,dom,skip) -> NDestructTac.destruct_tac dom skip
   | GrafiteAst.NDot _ -> NTactics.dot_tac 
   | GrafiteAst.NElim (_loc, what, where) ->
@@ -309,7 +403,7 @@ let eval_ng_tac tac =
   | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
   | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac 
   | GrafiteAst.NTry (_,tac) -> NTactics.try_tac
-      (aux f (text, prefix_len, tac))
+      (f f (text, prefix_len, tac))
   | GrafiteAst.NAssumption _ -> NTactics.assumption_tac
   | GrafiteAst.NBlock (_,l) -> 
       NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
@@ -328,25 +422,82 @@ let subst_metasenv_and_fix_names status =
    status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
 ;;
 
+let is_proof_irrelevant context ty =
+  match
+    NCicReduction.whd ~subst:[] context
+     (NCicTypeChecker.typeof ~subst:[] ~metasenv:[] context ty)
+  with
+     NCic.Sort NCic.Prop -> true
+   | NCic.Sort _ -> false
+   | _ -> assert false
+;;
+
+let rec relevance_of ?(context=[]) ty =
+ match NCicReduction.whd ~subst:[] context ty with
+    NCic.Prod (n,s,t) ->
+     not (is_proof_irrelevant context s) ::
+      relevance_of ~context:((n,NCic.Decl s)::context) t
+  | _ -> []
+;;
+
+let compute_relevance uri =
+ function
+    NCic.Constant (_,name,bo,ty,attrs) ->
+     let relevance = relevance_of ty in
+      NCic.Constant (relevance,name,bo,ty,attrs)
+  | NCic.Fixpoint (ind,funs,attrs) ->
+     let funs =
+       List.map
+       (fun (_,name,recno,ty,bo) ->
+         let relevance = relevance_of ty in
+          relevance,name,recno,ty,bo
+        ) funs
+     in
+      NCic.Fixpoint (ind,funs,attrs)
+  | NCic.Inductive (ind,leftno,tys,attrs) ->
+     let context =
+      List.rev_map (fun (_,name,arity,_) -> name,NCic.Decl arity) tys in
+     let tysno = List.length tys in
+     let tys =
+       List.map
+        (fun (_,name,arity,cons) ->
+         let relevance = relevance_of arity in
+         let cons =
+          List.map
+           (fun (_,name,ty) ->
+             let dety =
+               NCicTypeChecker.debruijn uri tysno ~subst:[] [] ty in
+             let relevance = relevance_of ~context dety in
+              relevance,name,ty
+           ) cons
+         in
+          (relevance,name,arity,cons)
+        ) tys
+     in
+      NCic.Inductive (ind,leftno,tys,attrs)
+;;
+
 
 let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
   match cmd with
   | GrafiteAst.Include (loc, mode, fname) ->
 	   let _root, baseuri, _fullpath, _rrelpath = 
        Librarian.baseuri_of_script ~include_paths fname in
+     let baseuri = NUri.uri_of_string baseuri in
+     (* MATITA 1.0: keep WithoutPreferences? *)
+     let alias_only = (mode = GrafiteAst.OnlyPreferences) in
      let status,obj =
-       GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
-        status in
+      GrafiteTypes.Serializer.require ~alias_only ~baseuri status in
      let status = status#set_dump (obj::status#dump) in
-     assert false; (* mode must be passed to GrafiteTypes.Serializer.require
-     somehow *)
+     let status = status#set_dependencies (fname::status#dependencies) in
        status
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
   | GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
      let status, composites =
-      NCicCoercDeclaration.eval_ncoercion status name t ty source target
-     in
-      LexiconSync.add_aliases_for_objs status composites
+      NCicCoercDeclaration.eval_ncoercion status name t ty source target in
+     let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
+     let aliases = GrafiteDisambiguate.aliases_for_objs composites in
+      eval_alias status (mode,aliases)
   | GrafiteAst.NQed loc ->
      if status#ng_mode <> `ProofMode then
       raise (GrafiteTypes.Command_error "Not in proof mode")
@@ -378,6 +529,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
               NCicUntrusted.map_obj_kind (fix ()) obj_kind 
           | _ -> obj_kind
         in
+        let obj_kind = compute_relevance uri obj_kind in
         let obj = uri,height,[],[],obj_kind in
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in
@@ -416,7 +568,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
            let uris = uri::List.rev uris_rev in
 *)
            let status = status#set_ng_mode `CommandMode in
-           let status = LexiconSync.add_aliases_for_objs status [uri] in
+           let xxaliases = GrafiteDisambiguate.aliases_for_objs [uri] in
+           let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
+           let status = eval_alias status (mode,xxaliases) in
            let status =
             List.fold_left
              (fun status boxml ->
@@ -479,15 +633,15 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
              (fun status (name,cpos,arity) ->
                try
                  let metasenv,subst,status,t =
-                  GrafiteDisambiguate.disambiguate_nterm None status [] [] []
+                  GrafiteDisambiguate.disambiguate_nterm status None [] [] []
                    ("",0,NotationPt.Ident (name,None)) in
                  assert (metasenv = [] && subst = []);
                  let status, nuris = 
                    NCicCoercDeclaration.
                      basic_eval_and_record_ncoercion_from_t_cpos_arity 
-                      status (name,t,cpos,arity)
-                 in
-                  LexiconSync.add_aliases_for_objs status nuris
+                      status (name,t,cpos,arity) in
+                 let aliases = GrafiteDisambiguate.aliases_for_objs nuris in
+                  eval_alias status (mode,aliases)
                with MultiPassDisambiguator.DisambiguationError _-> 
                  HLog.warn ("error in generating coercion: "^name);
                  status) 
@@ -571,7 +725,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       let metasenv,subst,status,sort = match sort with
         | None -> [],[],status,NCic.Sort NCic.Prop
         | Some s ->
-           GrafiteDisambiguate.disambiguate_nterm None status [] [] []
+           GrafiteDisambiguate.disambiguate_nterm status None [] [] []
             (text,prefix_len,s) 
       in
       assert (metasenv = []);
@@ -585,7 +739,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
              (NCicPp.ppterm ~metasenv ~subst ~context:[] sort))) in
       let status = status#set_ng_mode `ProofMode in
       let metasenv,subst,status,indty =
-       GrafiteDisambiguate.disambiguate_nterm None status [] [] subst
+       GrafiteDisambiguate.disambiguate_nterm status None [] [] subst
         (text,prefix_len,indty) in
       let indtyno,(_,leftno,tys,_,_) =
        match indty with
@@ -609,37 +763,10 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
       eval_add_constraint status [`Type,u1] [`Type,u2]
   (* ex lexicon commands *)
   | GrafiteAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
-     let rec disambiguate =
-      function
-         NotationPt.ApplPattern l ->
-          NotationPt.ApplPattern (List.map disambiguate l)
-       | NotationPt.VarPattern id
-          when not
-           (List.exists
-            (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
-          ->
-           let item = DisambiguateTypes.Id id in
-            begin
-             try
-              match
-               DisambiguateTypes.Environment.find item
-                status#lstatus.LexiconTypes.aliases
-              with
-                 GrafiteAst.Ident_alias (_, uri) ->
-                  NotationPt.NRefPattern (NReference.reference_of_string uri)
-               | _ -> assert false
-             with Not_found -> 
-              prerr_endline
-               ("LexiconEngine.eval_command: domain item not found: " ^ 
-               (DisambiguateTypes.string_of_domain_item item));
-              LexiconEngine.dump_aliases prerr_endline "" status;
-              raise 
-               (Failure
-                ((DisambiguateTypes.string_of_domain_item item) ^ " not found"))
-	          end
-       | p -> p
+     let cic_appl_pattern =
+      GrafiteDisambiguate.disambiguate_cic_appl_pattern status args
+       cic_appl_pattern
      in
-     let cic_appl_pattern = disambiguate cic_appl_pattern in
       eval_interpretation status (dsc,(symbol, args),cic_appl_pattern)
   | GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) ->
       let l1 = 
@@ -647,15 +774,10 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
          l1 (dir = Some `RightToLeft) precedence associativity
       in
       let status =
-        if dir <> Some `RightToLeft then
-          GrafiteParser.extend status l1 
-            (fun env loc ->
-              NotationPt.AttributedTerm
-               (`Loc loc,TermContentPres.instantiate_level2 env l2)) 
+        if dir <> Some `RightToLeft then eval_input_notation status (l1,l2)
         else status
       in
-       if dir <> Some `LeftToRight then
-        TermContentPres.add_pretty_printer status l2 l1
+       if dir <> Some `LeftToRight then eval_output_notation status (l1,l2)
        else status
   | GrafiteAst.Alias (loc, spec) -> 
      let diff =
@@ -670,8 +792,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
          [DisambiguateTypes.Num instance,spec]
      in
       let mode = GrafiteAst.WithPreferences in(*assert false in (* VEDI SOPRA *) MATITA 1.0*)
-      LexiconEngine.set_proof_aliases status ~implicit_aliases:false mode diff
-      (* assert false (* MANCA SALVATAGGIO SU DISCO *) *)
+       eval_alias status (mode,diff)
 ;;
 
 let eval_comment opts status (text,prefix_len,c) = status