module Extend

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@142 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 491 insertions, 1 deletions

diff --git a/parsing/extend.ml4 b/parsing/extend.ml4
new file mode 100644
index 0000000000..682d060abe
--- /dev/null
+++ b/parsing/extend.ml4
@@ -0,0 +1,394 @@
+
+(* $Id$ *)
+
+open Util
+open Gramext
+open Pp
+open Pcoq
+open Coqast
+open Ast
+
+open Vernac
+
+GEXTEND Gram
+  vernac:
+    [ RIGHTA
+     [ "Drop"; "." -> <:ast< (DROP) >>
+     | "ProtectedLoop"; "." -> <:ast< (PROTECTEDLOOP)>>
+     | "Load"; verbosely = [ IDENT "Verbose" -> "Verbose" | -> "" ];
+       s = [ s = STRING -> s | s = IDENT -> s ]; "." ->
+         <:ast< (LoadFile ($STR $verbosely) ($STR $s)) >>
+
+     (* TODO: deplacer vers g_vernac & Vernac.v *)
+     | "Compile";
+       verbosely =
+         [ IDENT "Verbose" -> "Verbose"
+         | -> "" ];
+       IDENT "Module";
+       only_spec =
+         [ IDENT "Specification" -> "Specification"
+         | -> "" ];
+       mname = [ s = STRING -> s | s = IDENT -> s ];
+       fname = OPT [ s = STRING -> s | s = IDENT -> s ]; "." ->
+         let fname = match fname with Some s -> s | None -> mname in
+         <:ast< (CompileFile ($STR $verbosely) ($STR $only_spec)
+                   ($STR $mname) ($STR $fname))>> ]]
+  ;
+END
+
+(* These are the entries without which MakeBare cannot be compiled *)
+GEXTEND Gram
+  GLOBAL: vernac Prim.syntax_entry Prim.grammar_entry;
+
+  vernac:
+    [[ "Token"; s = STRING; "." -> <:ast< (TOKEN ($STR $s)) >>
+
+     | "Grammar"; univ=IDENT; tl=LIST1 Prim.grammar_entry SEP "with"; "." ->
+         <:ast< (GRAMMAR ($VAR univ) (ASTLIST ($LIST tl))) >>
+
+     | "Syntax"; whatfor=IDENT; el=LIST1 Prim.syntax_entry SEP ";"; "." ->
+         <:ast< (SYNTAX ($VAR whatfor) (ASTLIST ($LIST el))) >>
+     | IDENT "Infix"; as_ = entry_prec; n = numarg; op = Prim.string;
+       p = identarg; "." -> <:ast< (INFIX (AST $as_) $n $op $p) >>
+     | IDENT "Distfix"; as_ = entry_prec; n = numarg; s = Prim.string;
+       p = identarg; "." -> <:ast< (DISTFIX (AST $as_) $n $s $p) >> ]]
+  ;
+
+  (* Syntax entries for Grammar. Only grammar_entry is exported *)
+  Prim.grammar_entry:
+    [[ nont = Prim.ident; etyp = Prim.entry_type; ":=";
+       ep = entry_prec; rl = LIST0 grammar_rule SEP "|" ->
+         <:ast< (ENTRY $nont $etyp $ep ($LIST rl)) >> ]]
+  ;
+  entry_prec:
+    [[ IDENT "LEFTA" -> <:ast< {LEFTA} >>
+     | IDENT "RIGHTA" -> <:ast< {RIGHTA} >>
+     | IDENT "NONA" -> <:ast< {NONA} >>
+     | ->  <:ast< {NONE} >> ] ]
+  ;
+  grammar_rule:
+    [[ name = rule_name; "["; pil = LIST0 production_item; "]"; "->";
+       a = Prim.astact ->
+        <:ast< (RULE ($ID name) $a ($LIST pil)) >> ]]
+  ;
+  rule_name:
+    [[ name = IDENT -> name ]]
+  ;
+  production_item:
+    [[ s = STRING -> <:ast< ($STR $s) >>
+     | nt = non_terminal; po = OPT [ "("; p = Prim.ident; ")" -> p ] ->
+         match po with
+           | Some p -> <:ast< (NT $nt $p) >>
+           | _ -> <:ast< (NT $nt) >> ]]
+  ;
+  non_terminal:
+    [[ u = Prim.ident; ":"; nt = Prim.ident -> <:ast< (QUAL $u $nt) >>
+     | nt = Prim.ident -> <:ast< $nt >> ]]
+  ;
+
+
+  (* Syntax entries for Syntax. Only syntax_entry is exported *)
+  Prim.syntax_entry:
+    [ [ IDENT "level"; p = precedence; ":"; rl = LIST1 syntax_rule SEP "|" ->
+          <:ast< (SYNTAXENTRY $p ($LIST $rl)) >> ] ]
+  ;
+  syntax_rule:
+    [ [ nm = IDENT; "["; s = Prim.astpat; "]"; "->"; u = unparsing ->
+          <:ast< (RULE ($ID $nm) $s $u) >> ] ]
+  ;
+  precedence:
+    [ [ a = Prim.number ->  <:ast< (PREC $a 0 0) >>
+      | "["; a1 = Prim.number; a2 = Prim.number; a3 = Prim.number; "]" ->
+          <:ast< (PREC $a1 $a2 $a3) >> ] ]
+  ;
+  unparsing:
+    [ [ "["; ll = LIST0 next_hunks; "]" -> <:ast< (UNPARSING ($LIST $ll))>> ] ]
+  ;
+  next_hunks:
+    [ [ IDENT "FNL" -> <:ast< (UNP_FNL) >>
+      | IDENT "TAB" -> <:ast< (UNP_TAB) >>
+      | c = STRING -> <:ast< (RO ($STR $c)) >>
+      | "[";
+        x =
+          [ b = box; ll = LIST0 next_hunks -> <:ast<(UNP_BOX $b ($LIST $ll))>>
+          | n = Prim.number; m = Prim.number -> <:ast< (UNP_BRK $n $m) >>
+          | IDENT "TBRK";
+            n = Prim.number; m = Prim.number -> <:ast< (UNP_TBRK $n $m) >> ];
+        "]" -> x
+      | e = Prim.ast; oprec = OPT [ ":"; pr = paren_reln -> pr ] ->
+            match oprec with
+	      | Some pr -> <:ast< (PH $e $pr) >>
+              | None -> <:ast< (PH $e {Any}) >> ]]
+  ;
+  box:
+    [ [ "<"; bk = box_kind; ">" -> bk ] ]
+  ;
+  box_kind:
+    [ [ IDENT "h"; n = Prim.number -> <:ast< (PpHB $n) >>
+      | IDENT "v"; n = Prim.number -> <:ast< (PpVB $n) >>
+      | IDENT "hv"; n = Prim.number -> <:ast< (PpHVB $n) >>
+      | IDENT "hov"; n = Prim.number -> <:ast< (PpHOVB $n) >>
+      | IDENT "t" -> <:ast< (PpTB) >> ] ]
+  ;
+  paren_reln:
+    [ [ IDENT "L" -> <:ast< {L} >>
+      | IDENT "E" -> <:ast< {E} >>
+      | pprim = STRING -> <:ast< ($STR $pprim) >> ] ]
+  ;
+END
+
+
+
+(* Converting and checking grammar command *)
+
+type nonterm =
+  | NtShort of string
+  | NtQual of string * string
+
+type prod_item =
+  | Term of Token.pattern
+  | NonTerm of nonterm * entry_type * string option
+
+type grammar_rule = {
+  gr_name : string; 
+  gr_production : prod_item list; 
+  gr_action : Ast.act }
+
+type grammar_entry = { 
+  ge_name : string;
+  ge_type : entry_type;
+  gl_assoc : g_assoc option;
+  gl_rules : grammar_rule list }
+
+type grammar_command = { 
+  gc_univ : string; 
+  gc_entries : grammar_entry list }
+
+let is_ident_not_keyword s =
+  match s.[0] with
+    | 'a'..'z' | 'A'..'Z' | '_' -> not (Lexer.is_keyword s)
+    | _ -> false
+
+let is_number s =
+  match s.[0] with
+    | '0'..'9' -> true
+    | _ -> false
+
+let strip s =
+  let len =
+    let rec loop i len =
+      if i = String.length s then len
+      else if s.[i] == ' ' then loop (i + 1) len
+      else loop (i + 1) (len + 1)
+    in
+    loop 0 0
+  in
+  if len == String.length s then s
+  else
+    let s' = String.create len in
+    let rec loop i i' =
+      if i == String.length s then s'
+      else if s.[i] == ' ' then loop (i + 1) i'
+      else begin s'.[i'] <- s.[i]; loop (i + 1) (i' + 1) end
+    in
+    loop 0 0
+
+let terminal s =
+  let s = strip s in
+  if s = "" then failwith "empty token";
+  if is_ident_not_keyword s then ("IDENT", s)
+  else if is_number s then ("INT", s)
+  else ("", s)
+
+
+
+let qualified_nterm current_univ ntrm =
+  match ntrm with
+      NtQual (univ, en) -> (get_univ univ, en)
+    | NtShort en -> (current_univ, en)
+
+
+let nterm univ ast =
+  let nont =
+    match ast with
+      | Node (_, "QUAL", [Id (_, u); Id (_, nt)]) -> NtQual (u, nt)
+      | Id (_, nt) -> NtShort nt
+      | _ -> invalid_arg_loc (Ast.loc ast, "Extend.nterm") 
+  in
+  let (u,n) = qualified_nterm univ nont in
+  let e =
+    try 
+      get_entry u n
+    with UserError _ -> 
+      user_err_loc(loc ast,"Externd.nterm", [< 'sTR"unknown grammar entry" >])
+  in
+  (nont, type_of_entry e)
+
+let prod_item univ env ast =
+  match ast with
+    | Str (_, s) -> env, Term (terminal s)
+    | Node (_, "NT", [nt; Id (locp, p)]) ->
+	let (nont, etyp) = nterm univ nt in
+        if isMeta p then 
+	  ((p, etyp) :: env, NonTerm (nont, etyp, Some p))
+        else 
+	  user_err_loc
+            (locp,"Extend.prod_item",
+             [< 'sTR"This ident is not a metavariable." >])
+    | Node (_, "NT", [nt]) ->
+	let (nont, etyp) = nterm univ nt in 
+	env, NonTerm (nont, etyp, None)
+    | _ -> invalid_arg_loc (Ast.loc ast, "Extend.prod_item")
+
+let rec prod_item_list univ penv pil =
+  match pil with
+    | [] -> [], penv
+    | pi :: pitl ->
+	let (env, pic) = prod_item univ penv pi in
+	let (pictl, act_env) = prod_item_list univ env pitl in
+        (pic :: pictl, act_env)
+
+let gram_rule univ etyp ast =
+  match ast with
+    | Node (_, "RULE", (Id (_, name) :: act :: pil)) ->
+	let (pilc, act_env) = prod_item_list univ [] pil in
+	let a = Ast.to_act_check_vars act_env etyp act in
+        { gr_name=name; gr_production=pilc; gr_action=a }
+    | _ -> invalid_arg_loc (Ast.loc ast, "Extend.gram_rule")
+
+let gram_entry univ (nt, etyp, ass, rl) =
+  { ge_name = nt;
+    ge_type = etyp;
+    gl_assoc = ass;
+    gl_rules = List.map (gram_rule univ etyp) rl }
+
+let gram_assoc = function
+  | Id (_, "LEFTA") -> Some LeftA
+  | Id (_, "RIGHTA") -> Some RightA
+  | Id (_, "NONA") -> Some NonA
+  | Id (_, "NONE") -> None
+  | ast -> invalid_arg_loc (Ast.loc ast, "Egrammar.assoc")
+
+let gram_define_entry univ = function
+  | Node (_, "ENTRY", (Id (ntl, nt) :: et :: ass :: rl)) ->
+      let etyp = entry_type et in
+      let assoc = gram_assoc ass in
+      let _ =
+        try 
+	  create_entry univ nt etyp
+        with Failure s ->
+          user_err_loc (ntl,"Extend.gram_define_entry",[< 'sTR s >])
+      in 
+      (nt, etyp, assoc, rl)
+  | ast -> invalid_arg_loc (Ast.loc ast, "Egrammar.gram_define_entry")
+
+let gram_of_ast univ astl =
+  let u = get_univ univ in
+  let entryl = List.map (gram_define_entry u) astl in
+  { gc_univ = univ;
+    gc_entries = List.map (gram_entry u) entryl }
+
+
+(* Converting and checking pretty-printing command *)
+
+type parenRelation = L | E | Any
+type precedence = int * int * int
+
+let compare_prec (a1,b1,c1) (a2,b2,c2) =
+  match (a1=a2),(b1=b2),(c1=c2) with
+    | true,true,true -> 0
+    | true,true,false -> c1-c2
+    | true,false,_ -> b1-b2
+    | false,_,_ -> a1-a2
+
+let tolerable_prec oparent_prec_reln (_,child_prec) =
+  match oparent_prec_reln with
+    | Some ((_,pprec), L) -> (compare_prec child_prec pprec) < 0
+    | Some ((_,pprec), E) -> (compare_prec child_prec pprec) <= 0
+    | _ -> true
+
+type ppbox =
+  | PpHB of int
+  | PpHOVB of int
+  | PpHVB of int
+  | PpVB of int
+  | PpTB
+
+type unparsing_hunk = 
+  | PH of Ast.pat * string option * parenRelation
+  | RO of string
+  | UNP_BOX of ppbox * unparsing_hunk list
+  | UNP_BRK of int * int
+  | UNP_TBRK of int * int
+  | UNP_TAB
+  | UNP_FNL
+
+let ppcmd_of_box = function
+  | PpHB n -> h n
+  | PpHOVB n -> hOV n
+  | PpHVB n -> hV n
+  | PpVB n -> v n
+  | PpTB   -> t
+
+(* Parsing the unparsing specifications *)
+
+let box_of_ast = function
+  | Node (_, "PpHB", [Num (_, n)]) -> (PpHB n)
+  | Node (_, "PpHOVB", [Num (_, n)]) -> (PpHOVB n)
+  | Node (_, "PpHVB", [Num (_, n)]) -> (PpHVB n)
+  | Node (_, "PpVB", [Num (_, n)]) -> (PpVB n)
+  | Node (_, "PpTB", [])           -> PpTB
+  | p -> invalid_arg_loc (Ast.loc p,"Syntaxext.box_of_ast")
+
+let rec unparsing_hunk_of_ast vars = function
+  | Node(_, "PH", [e; Str(_,pprim)]) ->
+      PH (Ast.val_of_ast vars e, Some pprim, Any)
+  | Node(loc, "PH", [e; Id(_,pr)]) ->
+      let reln =
+        (match pr with
+           | "L" -> L
+           | "E" -> E
+           | "Any" -> Any 
+           | _ -> invalid_arg_loc (loc,"Syntaxext.paren_reln_of_ast")) in
+      PH (Ast.val_of_ast vars e, None, reln)
+  | Node (_, "RO", [Str(_,s)]) -> RO s
+  | Node (_, "UNP_FNL", []) -> UNP_FNL
+  | Node (_, "UNP_TAB", []) -> UNP_TAB
+  | Node (_, "UNP_BRK", [Num(_, n1); Num(_, n2)]) -> UNP_BRK(n1,n2)
+  | Node (_, "UNP_TBRK", [Num(_, n1); Num(_, n2)]) -> UNP_TBRK(n1,n2)
+  | Node (_, "UNP_BOX", (box::sub)) ->
+      UNP_BOX(box_of_ast box,
+              List.map (unparsing_hunk_of_ast vars) sub)
+  | h -> invalid_arg_loc (Ast.loc h,"Syntaxext.unparsing_hunk_of_ast")
+
+let unparsing_of_ast vars = function
+  | Node(_,"UNPARSING",ll) ->
+      List.map (unparsing_hunk_of_ast vars) ll
+  | u -> invalid_arg_loc (Ast.loc u,"Syntaxext.unp_of_ast")
+
+let prec_of_ast = function
+  | Node(_,"PREC",[Num(_,a1); Num(_,a2); Num(_,a3)]) -> (a1,a2,a3)
+  | ast -> invalid_arg_loc (Ast.loc ast,"Syntaxext.prec_of_ast")
+
+
+type syntax_entry = {
+  syn_id : string;
+  syn_prec: precedence;
+  syn_astpat : Ast.pat;
+  syn_hunks : unparsing_hunk list }
+
+let rule_of_ast whatfor prec = function
+  | Node(_,"RULE",[Id(_,s); spat; unp]) ->
+      let (astpat,meta_env) = Ast.to_pat [] spat in
+      let hunks = unparsing_of_ast meta_env unp in
+      { syn_id = s;
+	syn_prec = prec;
+        syn_astpat = astpat;
+        syn_hunks = hunks }
+  | ast -> invalid_arg_loc (Ast.loc ast,"Metasyntax.rule_of_ast")
+
+let level_of_ast whatfor = function
+  | Node(_,"SYNTAXENTRY",(pr::rl)) ->
+      let prec = prec_of_ast pr in
+      List.map (rule_of_ast whatfor prec) rl
+  | ast -> invalid_arg_loc (Ast.loc ast,"Metasyntax.level_of_ast")
diff --git a/parsing/extend.mli b/parsing/extend.mli
new file mode 100644
index 0000000000..7f9a5f5699
--- /dev/null
+++ b/parsing/extend.mli
@@ -0,0 +1,90 @@
+
+(* $Id$ *)
+
+(*i*)
+open Pp
+open Pcoq
+(*i*)
+
+(* Parsing. *)
+
+type nonterm =
+  | NtShort of string
+  | NtQual of string * string
+
+val qualified_nterm : (string * gram_universe) -> nonterm ->
+  (string * gram_universe) * string
+
+type prod_item =
+  | Term of Token.pattern
+  | NonTerm of nonterm * entry_type * string option
+
+type grammar_rule = { 
+  gr_name : string; 
+  gr_production : prod_item list; 
+  gr_action : Ast.act }
+
+type grammar_entry = { 
+  ge_name : string;
+  ge_type : entry_type;
+  gl_assoc : Gramext.g_assoc option;
+  gl_rules : grammar_rule list }
+
+type grammar_command = { 
+  gc_univ : string; 
+  gc_entries : grammar_entry list }
+
+val gram_assoc: Coqast.t -> Gramext.g_assoc option
+val gram_of_ast: string -> Coqast.t list -> grammar_command
+
+
+(*s Pretty-print. *)
+
+(* Dealing with precedences *)
+
+type precedence = int * int * int
+
+type parenRelation = L | E | Any
+
+(* Checks if the precedence of the parent printer (None means the
+   highest precedence), and the child's one, follow the given
+   relation. *)
+
+val tolerable_prec : ((string * precedence) * parenRelation) option ->
+  (string * precedence) -> bool
+
+val prec_of_ast : Coqast.t -> precedence
+
+(* unparsing objects *)
+
+type ppbox =
+  | PpHB of int
+  | PpHOVB of int
+  | PpHVB of int
+  | PpVB of int
+  | PpTB
+
+type unparsing_hunk = 
+  | PH of Ast.pat * string option * parenRelation
+  | RO of string
+  | UNP_BOX of ppbox * unparsing_hunk list
+  | UNP_BRK of int * int
+  | UNP_TBRK of int * int
+  | UNP_TAB
+  | UNP_FNL
+
+val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds
+
+val unparsing_of_ast : Ast.entry_env -> Coqast.t -> unparsing_hunk list
+
+type syntax_entry = {
+  syn_id : string;
+  syn_prec: precedence;
+  syn_astpat : Ast.pat;
+  syn_hunks : unparsing_hunk list }
+
+val rule_of_ast : string -> precedence -> Coqast.t -> syntax_entry
+
+val level_of_ast : string -> Coqast.t -> syntax_entry list
+
+
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index cbc4bc49e0..72ee09b1c1 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -2,6 +2,8 @@
 (* $Id$ *)
 
 val add_keyword : string -> unit
+val is_keyword : string -> bool
+val find_keyword : string -> string
 
 val func : char Stream.t -> (string * string) Stream.t * (int -> int * int)
 
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index c185a03430..cc0f8856c4 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -23,6 +23,8 @@ let add_keyword,is_keyword =
       "Prop"; "Set"; "Type" ];
   (fun s -> Hashtbl.add table s ()),
   (fun s -> try Hashtbl.find table s; true with Not_found -> false)
+
+let find_keyword s = if is_keyword s then s else raise Not_found
       
 let char_for_backslash =
   match Sys.os_type with
diff --git a/parsing/printer.mli b/parsing/printer.mli
index bcdc6f93a7..9bf72b6600 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -5,6 +5,7 @@
 open Pp
 open Names
 open Term
+open Sign
 (*i*)
 
 val gencompr  : path_kind -> Coqast.t -> std_ppcmds
diff --git a/parsing/termast.mli b/parsing/termast.mli
index 1ef1dbf1ac..06cab8244c 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -2,8 +2,9 @@
 (* $Id$ *)
 
 (*i*)
-open Term
 open Names
+open Term
+open Sign
 (*i*)
 
 (* Translation of terms into syntax trees. Used for pretty-printing. *)