helm/ocaml/cic_disambiguation/parser.ml

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 let debug = true
  27 let debug_print s =
  28   if debug then begin
  29     prerr_endline "<NEW_TEXTUAL_PARSER>";
  30     prerr_endline s;
  31     prerr_endline "</NEW_TEXTUAL_PARSER>"
  32   end
  33
  34 let grammar = Grammar.gcreate Lexer.lex
  35
  36 let term = Grammar.Entry.create grammar "term"
  37 (* let tactic = Grammar.Entry.create grammar "tactic" *)
  38 (* let tactical = Grammar.Entry.create grammar "tactical" *)
  39
  40 let return_term loc term = Ast.LocatedTerm (loc, term)
  41 (* let return_term loc term = term *)
  42
  43 let fail (x, y) msg =
  44   failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
  45
  46 EXTEND
  47   GLOBAL: term;
  48   meta_subst: [
  49     [ s = SYMBOL "_" -> None
  50     | t = term -> Some t ]
  51   ];
  52   binder: [
  53     [ SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
  54     | SYMBOL <:unicode<pi>> (* π *) -> `Pi
  55     | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
  56     | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
  57     ]
  58   ];
  59   substituted_name: [ (* a subs.name is an explicit substitution subject *)
  60     [ s = [ IDENT | SYMBOL ];
  61       subst = OPT [
  62         SYMBOL "\subst";  (* to avoid catching frequent "a [1]" cases *)
  63         LPAREN "[";
  64         substs = LIST1 [
  65           i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
  66         ] SEP SYMBOL ";";
  67         RPAREN "]" ->
  68           substs
  69       ] ->
  70         (match subst with
  71         | Some l -> Ast.Ident (s, l)
  72         | None -> Ast.Ident (s, []))
  73     ]
  74   ];
  75   name: [ (* as substituted_name with no explicit substitution *)
  76     [ s = [ IDENT | SYMBOL ] -> s ]
  77   ];
  78   pattern: [
  79     [ n = name -> [n]
  80     | LPAREN "("; names = LIST1 name; RPAREN ")" -> names ]
  81   ];
  82   term:
  83     [ "arrow" RIGHTA
  84       [ t1 = term; SYMBOL <:unicode<to>>; t2 = term ->
  85           return_term loc (Ast.Binder (`Pi, Cic.Anonymous, Some t1, t2))
  86       ]
  87     | "eq" LEFTA
  88       [ t1 = term; SYMBOL "="; t2 = term ->
  89         return_term loc (Ast.Appl_symbol ("eq", [t1; t2]))
  90       ]
  91     | "add" LEFTA     [ (* nothing here by default *) ]
  92     | "mult" LEFTA    [ (* nothing here by default *) ]
  93     | "inv" NONA      [ (* nothing here by default *) ]
  94     | "simple" NONA
  95       [
  96         b = binder; vars = LIST1 IDENT SEP SYMBOL ",";
  97         typ = OPT [ SYMBOL ":"; t = term -> t ];
  98         SYMBOL "."; body = term ->
  99           let binder =
 100             List.fold_right
 101               (fun var body -> Ast.Binder (b, Cic.Name var, typ, body))
 102               vars body
 103           in
 104           return_term loc binder
 105       | sort_kind = [
 106           "Prop" -> `Prop | "Set" -> `Set | "Type" -> `Type | "CProp" -> `CProp
 107         ] ->
 108           Ast.Sort sort_kind
 109       | n = substituted_name -> return_term loc n
 110       | LPAREN "("; head = term; args = LIST1 term; RPAREN ")" ->
 111           return_term loc (Ast.Appl (head :: args))
 112       | i = INT -> return_term loc (Ast.Num i)
 113       | m = META;
 114         substs = [
 115           LPAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; RPAREN "]" ->
 116             substs
 117         ] ->
 118             let index =
 119               try
 120                 int_of_string (String.sub m 1 (String.length m - 1))
 121               with Failure "int_of_string" ->
 122                 fail loc ("Invalid meta variable number: " ^ m)
 123             in
 124             return_term loc (Ast.Meta (index, substs))
 125         (* actually "in" and "and" are _not_ keywords. Parsing works anyway
 126          * since applications are required to be bound by parens *)
 127       | "let"; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *); t1 = term;
 128         IDENT "in"; t2 = term ->
 129           return_term loc (Ast.LetIn (name, t1, t2))
 130       | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
 131           defs = LIST1 [
 132           name = IDENT;
 133           index = OPT [ LPAREN "("; index = INT; RPAREN ")" ->
 134             int_of_string index
 135           ];
 136           typ = OPT [ SYMBOL ":"; typ = term -> typ ];
 137           SYMBOL <:unicode<def>> (* ≝ *); t1 = term ->
 138             (name, t1, typ, (match index with None -> 1 | Some i -> i))
 139         ] SEP (IDENT "and");
 140         IDENT "in"; body = term ->
 141           return_term loc (Ast.LetRec (ind_kind, defs, body))
 142       | outtyp = OPT [ LPAREN "["; typ = term; RPAREN "]" -> typ ];
 143         "match"; t = term;
 144         SYMBOL ":"; indty = IDENT;
 145         "with";
 146         LPAREN "[";
 147         patterns = LIST0 [
 148           p = pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *); t = term -> (p, t)
 149         ] SEP SYMBOL "|";
 150         RPAREN "]" ->
 151           return_term loc (Ast.Case (t, indty, outtyp, patterns))
 152       | LPAREN "("; t = term; RPAREN ")" -> return_term loc t
 153       ]
 154     ];
 155 END
 156
 157 let parse_term = Grammar.Entry.parse term
 158
 159 (*
 160 open Disambiguate_struct
 161 open ProofEngineHelpers
 162
 163 exception UnknownIdentifier of string
 164 exception InductiveTypeExpected
 165
 166 let list_of_domain dom = Domain.fold (fun s acc -> s :: acc) dom []
 167 let apply_interp (interp: interpretation) item = snd (interp item)
 168
 169 let pre_disambiguate ~context ast =
 170   let rec aux loc context = function
 171     | Ast.LocatedTerm (loc, term) -> aux loc context term
 172     | Ast.Appl terms ->
 173         let (dom, funs) =
 174           List.fold_left
 175             (fun (dom, funs) term ->
 176               let (dom', f) = aux loc context term in
 177               (Domain.union dom dom', f :: funs))
 178             (Domain.empty, [])
 179             terms
 180         in
 181         let f interp =
 182           Cic.Appl (List.map (fun f -> f interp) (List.rev funs))
 183         in
 184         (dom, f)
 185     | Ast.Appl_symbol (symb, args) ->
 186         let (dom, funs) =
 187           List.fold_left
 188             (fun (dom, funs) term ->
 189               let (dom', f) = aux loc context term in
 190               (Domain.union dom dom', f :: funs))
 191             (Domain.empty, [])
 192             args
 193         in
 194         (Domain.add (Symbol (symb, 0)) dom,
 195          (fun interp ->
 196            apply_interp interp (Symbol (symb, 0)) interp
 197             (List.map (fun f -> f interp) funs)))
 198     | Ast.Binder (binder_kind, var, typ, body) ->
 199         let (type_dom, type_f) =
 200           match typ with
 201           | Some t -> aux loc context t
 202           | None -> (Domain.empty, (fun _ -> Cic.Implicit))
 203         in
 204         let (dom', body_f) = aux loc (Some var :: context) body in
 205         let dom'' = Domain.union dom' type_dom in
 206         (dom'',
 207          match binder_kind with
 208          | `Lambda ->
 209              (fun interp ->
 210                Cic.Lambda (var, type_f interp, body_f interp))
 211          | `Pi | `Forall ->
 212              (fun interp ->
 213                Cic.Prod (var, type_f interp, body_f interp))
 214          | `Exists ->
 215              (fun interp ->
 216                let typ = type_f interp in
 217                Cic.Appl
 218                 [ apply_interp interp (Id "ex") interp [];
 219                   typ;
 220                   (Cic.Lambda (var, typ, body_f interp)) ]))
 221     | Ast.Case (term, indty_ident, outtype, branches) ->
 222         let (term_dom, term_f) = aux loc context term in
 223         let (outtype_dom, outtype_f) =
 224           match outtype with
 225           | Some typ -> aux loc context typ
 226           | None -> (Domain.empty, (fun _ -> Cic.Implicit))
 227         in
 228         let do_branch (pat, term) =
 229           let rec do_branch' context = function
 230             | [] -> aux loc context term
 231             | hd :: tl ->
 232                 let (dom, f) = do_branch' (Some (Cic.Name hd) :: context) tl in
 233                 (dom,
 234                  (fun interp ->
 235                    Cic.Lambda (Cic.Name hd, Cic.Implicit, f interp)))
 236           in
 237           match pat with
 238           | _ :: tl -> (* ignoring constructor *)
 239               do_branch' context tl
 240           | [] -> assert false
 241         in
 242         let (branches_dom, branches_f) =
 243           List.fold_right
 244             (fun branch (dom, f) ->
 245               let (dom', f') = do_branch branch in
 246               Domain.union dom dom', (fun interp -> f' interp :: f interp))
 247             branches
 248             (Domain.empty, (fun _ -> []))
 249         in
 250         (Domain.union outtype_dom (Domain.union term_dom branches_dom),
 251          (fun interp ->
 252            let (indtype_uri, indtype_no) =
 253              match apply_interp interp (Id indty_ident) interp [] with
 254              | Cic.MutInd (uri, tyno, _) -> uri, tyno
 255              | _ -> assert false
 256            in
 257            Cic.MutCase (indtype_uri, indtype_no, outtype_f interp,
 258             term_f interp, branches_f interp)))
 259     | Ast.LetIn (var, body, where) ->
 260         let (body_dom, body_f) = aux loc context body in
 261         let (where_dom, where_f) = aux loc context where in
 262         (Domain.union body_dom where_dom,
 263          fun interp -> Cic.LetIn (Cic.Name var, body_f interp, where_f interp))
 264     | Ast.LetRec (kind, defs, where) ->
 265         let context' =
 266           List.fold_left (fun acc (var, _, _, _) -> Some (Cic.Name var) :: acc)
 267             context defs
 268         in
 269         let (where_dom, where_f) = aux loc context' where in
 270         let inductiveFuns =
 271           List.map
 272             (fun (var, body, typ, decr_idx) ->
 273               let body_dom, body_f = aux loc context' body in
 274               let typ_dom, typ_f =
 275                 match typ with
 276                 | None -> (Domain.empty, (fun _ -> Cic.Implicit))
 277                 | Some typ -> aux loc context' typ
 278               in
 279               (Domain.union body_dom typ_dom,
 280                (fun interp ->
 281                  (var, decr_idx, typ_f interp, body_f interp))))
 282             defs
 283         in
 284         let dom =
 285           List.fold_left (fun acc (dom, _) -> Domain.union acc dom)
 286             where_dom inductiveFuns
 287         in
 288         let inductiveFuns interp =
 289           List.map (fun (_, g) -> g interp) inductiveFuns
 290         in
 291         let build_term counter funs =
 292           (* this is the body of the fold_right function below. Rationale: Fix
 293            * and CoFix cases differs only in an additional index in the
 294            * indcutiveFun list, see Cic.term *)
 295           match kind with
 296           | `Inductive ->
 297               (fun (var, _, _, _) cic ->
 298                 incr counter;
 299                 Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
 300           | `CoInductive ->
 301               let funs =
 302                 List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
 303               in
 304               (fun (var, _, _, _) cic ->
 305                 Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
 306         in
 307         (dom,
 308          (fun interp ->
 309            let counter = ref 0 in
 310            let funs = inductiveFuns interp in
 311            List.fold_right (build_term counter funs) funs (where_f interp)))
 312     | Ast.Ident (name, subst) ->
 313         (* TODO hanlde explicit substitutions *)
 314         let rec find acc e = function
 315           | [] -> raise Not_found
 316           | Some (Cic.Name hd) :: tl when e = hd -> acc
 317           | _ :: tl ->  find (acc + 1) e tl
 318         in
 319         (try
 320           let index = find 1 name context in
 321           if subst <> [] then
 322             fail loc "Explicit substitutions not allowed here";
 323           (Domain.empty, fun _ -> Cic.Rel index)
 324         with Not_found ->
 325           (Domain.singleton (Id name),
 326            (fun interp -> apply_interp interp (Id name) interp [])))
 327     | Ast.Num num ->
 328         (* TODO check to see if num can be removed from the domain *)
 329         (Domain.singleton (Num (num, 0)),
 330           (fun interp -> apply_interp interp (Num (num, 0)) interp []))
 331     | Ast.Meta (index, subst) ->
 332         let (dom, funs) =
 333           List.fold_left
 334             (fun (dom, funs) term ->
 335               match term with
 336               | None -> (dom, (fun _ -> None) :: funs)
 337               | Some term ->
 338                   let (dom', f) = aux loc context term in
 339                   (Domain.union dom dom',
 340                    (fun interp -> Some (f interp)) :: funs))
 341             (Domain.empty, [])
 342             subst
 343         in
 344         let f interp =
 345           Cic.Meta (index, List.map (fun f -> f interp) (List.rev funs))
 346         in
 347         (dom, f)
 348     | Ast.Sort `Prop -> Domain.empty, fun _ -> Cic.Sort Cic.Prop
 349     | Ast.Sort `Set -> Domain.empty, fun _ -> Cic.Sort Cic.Set
 350     | Ast.Sort `Type -> Domain.empty, fun _ -> Cic.Sort Cic.Type
 351     | Ast.Sort `CProp -> Domain.empty, fun _ -> Cic.Sort Cic.CProp
 352   in
 353   match ast with
 354   | Ast.LocatedTerm (loc, term) ->
 355       let (dom, f) = aux loc context term in
 356       dom, f
 357   | _ -> assert false
 358
 359 let main ~context char_stream =
 360   let term_ast = parse_term char_stream in
 361   debug_print (Pp.pp_term term_ast);
 362   pre_disambiguate ~context term_ast
 363 *)
 364