From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 12 Dec 2005 16:01:04 +0000 (+0000)
Subject: - coercion now requires an URI
X-Git-Tag: make_still_working~8014
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7a7af8e1ed42aa440476975ec918d38f0c3d13c9;p=helm.git

- coercion now requires an URI
- ported to new pattern type
---

diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
index 3c79cc040..7b6b69d44 100644
--- a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
@@ -69,7 +69,7 @@ let disambiguate_lazy_term status_ref term =
 
 let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
   let interp path = Disambiguate.interpretate_path [] path in
-  let goal_path = interp goal_path in
+  let goal_path = HExtlib.map_option interp goal_path in
   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
   let wanted =
    match wanted with
@@ -78,7 +78,7 @@ let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
        let wanted = disambiguate_lazy_term status_ref wanted in
        Some wanted
   in
-  (wanted, hyp_paths ,goal_path)
+  (wanted, hyp_paths, goal_path)
 
 let disambiguate_reduction_kind aliases_ref = function
   | `Unfold (Some t) ->
@@ -233,6 +233,7 @@ let disambiguate_obj status obj =
 let disambiguate_command status =
   function
   | GrafiteAst.Alias _
+  | GrafiteAst.Coercion _
   | GrafiteAst.Default _
   | GrafiteAst.Drop _
   | GrafiteAst.Dump _
@@ -243,10 +244,7 @@ let disambiguate_command status =
   | GrafiteAst.Render _
   | GrafiteAst.Set _ as cmd ->
       status,cmd
-  | GrafiteAst.Coercion (loc, term, add_composites) ->
-      let status_ref = ref status in
-      let term = disambiguate_term ~context:[] status_ref ~-1 term in
-      !status_ref, GrafiteAst.Coercion (loc,term,add_composites)
   | GrafiteAst.Obj (loc,obj) ->
       let status,obj = disambiguate_obj status obj in
       status, GrafiteAst.Obj (loc,obj)
+
diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.mli b/helm/ocaml/grafite_parser/grafiteDisambiguate.mli
index 21836853f..379b65c1e 100644
--- a/helm/ocaml/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.mli
@@ -32,5 +32,6 @@ val disambiguate_tactic:
 
 val disambiguate_command: 
  GrafiteTypes.status ->
-  (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command ->
-  GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command
+  CicNotationPt.obj GrafiteAst.command ->
+  GrafiteTypes.status * Cic.obj GrafiteAst.command
+
diff --git a/helm/ocaml/grafite_parser/grafiteParser.ml b/helm/ocaml/grafite_parser/grafiteParser.ml
index f76528567..aa60c87c4 100644
--- a/helm/ocaml/grafite_parser/grafiteParser.ml
+++ b/helm/ocaml/grafite_parser/grafiteParser.ml
@@ -72,9 +72,9 @@ EXTEND
      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
       let goal_path =
        match goal_path, hyp_paths with
-          None, [] -> Ast.UserInput
-        | None, _::_ -> Ast.Implicit
-        | Some goal_path, _ -> goal_path
+          None, [] -> Some Ast.UserInput
+        | None, _::_ -> None
+        | Some goal_path, _ -> Some goal_path
       in
        hyp_paths,goal_path
    ]
@@ -91,12 +91,12 @@ EXTEND
         ] ->
          let wanted,hyp_paths,goal_path =
           match wanted_and_sps with
-             wanted,None -> wanted, [], Ast.UserInput
+             wanted,None -> wanted, [], Some Ast.UserInput
            | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
          in
           wanted, hyp_paths, goal_path ] ->
       match res with
-         None -> None,[],Ast.UserInput
+         None -> None,[],Some Ast.UserInput
        | Some ps -> ps]
   ];
   direction: [
@@ -476,10 +476,8 @@ EXTEND
             ind_types
         in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
-    | IDENT "coercion" ; name = IDENT -> 
-        GrafiteAst.Coercion (loc, Ast.Ident (name,Some []), true)
-    | IDENT "coercion" ; name = URI -> 
-        GrafiteAst.Coercion (loc, Ast.Uri (name,Some []), true)
+    | IDENT "coercion" ; suri = URI ->
+        GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true)
     | IDENT "alias" ; spec = alias_spec ->
         GrafiteAst.Alias (loc, spec)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->