X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fparser.ml;h=13f9fc42d39addc2b8cc3f7abd5fa504bb129b32;hb=aba014724c9ad08f80944ec3021c9fa3826dca4a;hp=0ee41ab2afe0fc5f0a28afe25937044c0c0fd1c8;hpb=f0196d4e96bf8cc579d1690fc6a653adc08ca02e;p=helm.git
diff --git a/helm/ocaml/cic_disambiguation/parser.ml b/helm/ocaml/cic_disambiguation/parser.ml
index 0ee41ab2a..13f9fc42d 100644
--- a/helm/ocaml/cic_disambiguation/parser.ml
+++ b/helm/ocaml/cic_disambiguation/parser.ml
@@ -1,5 +1,35 @@
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
-open Ast
+let debug = true
+let debug_print s =
+ if debug then begin
+ prerr_endline "";
+ prerr_endline s;
+ prerr_endline ""
+ end
let grammar = Grammar.gcreate Lexer.lex
@@ -7,7 +37,11 @@ let term = Grammar.Entry.create grammar "term"
(* let tactic = Grammar.Entry.create grammar "tactic" *)
(* let tactical = Grammar.Entry.create grammar "tactical" *)
-let return_term loc term = LocatedTerm (loc, term)
+let return_term loc term = Ast.LocatedTerm (loc, term)
+(* let return_term loc term = term *)
+
+let fail (x, y) msg =
+ failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
EXTEND
GLOBAL: term;
@@ -34,8 +68,8 @@ EXTEND
substs
] ->
(match subst with
- | Some l -> Ident (s, l)
- | None -> Ident (s, []))
+ | Some l -> Ast.Ident (s, l)
+ | None -> Ast.Ident (s, []))
]
];
name: [ (* as substituted_name with no explicit substitution *)
@@ -46,35 +80,55 @@ EXTEND
| LPAREN "("; names = LIST1 name; RPAREN ")" -> names ]
];
term:
- [ "add" LEFTA [ (* nothing here by default *) ]
- | "mult" LEFTA [ (* nothing here by default *) ]
- | "inv" NONA [ (* nothing here by default *) ]
+ [ "arrow" RIGHTA
+ [ t1 = term; SYMBOL <:unicode>; t2 = term ->
+ return_term loc (Ast.Binder (`Pi, Cic.Anonymous, Some t1, t2))
+ ]
+ | "eq" LEFTA
+ [ t1 = term; SYMBOL "="; t2 = term ->
+ return_term loc (Ast.Appl_symbol ("eq", [t1; t2]))
+ ]
+ | "add" LEFTA [ (* nothing here by default *) ]
+ | "mult" LEFTA [ (* nothing here by default *) ]
+ | "inv" NONA [ (* nothing here by default *) ]
| "simple" NONA
[
b = binder; vars = LIST1 IDENT SEP SYMBOL ",";
typ = OPT [ SYMBOL ":"; t = term -> t ];
SYMBOL "."; body = term ->
let binder =
- List.fold_right (fun var body -> Binder (b, var, typ, body))
+ List.fold_right
+ (fun var body -> Ast.Binder (b, Cic.Name var, typ, body))
vars body
in
return_term loc binder
+ | sort_kind = [
+ "Prop" -> `Prop | "Set" -> `Set | "Type" -> `Type | "CProp" -> `CProp
+ ] ->
+ Ast.Sort sort_kind
| n = substituted_name -> return_term loc n
| LPAREN "("; head = term; args = LIST1 term; RPAREN ")" ->
- return_term loc (Appl (head :: args))
- | i = INT -> return_term loc (Int (int_of_string i))
+ return_term loc (Ast.Appl (head :: args))
+ | i = INT -> return_term loc (Ast.Num i)
| m = META;
substs = [
LPAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; RPAREN "]" ->
substs
] ->
- return_term loc (Meta (m, substs))
+ let index =
+ try
+ int_of_string (String.sub m 1 (String.length m - 1))
+ with Failure "int_of_string" ->
+ fail loc ("Invalid meta variable number: " ^ m)
+ in
+ return_term loc (Ast.Meta (index, substs))
(* actually "in" and "and" are _not_ keywords. Parsing works anyway
* since applications are required to be bound by parens *)
| "let"; name = IDENT; SYMBOL <:unicode> (* â *); t1 = term;
IDENT "in"; t2 = term ->
- return_term loc (LetIn (name, t1, t2))
- | "let"; "rec"; defs = LIST1 [
+ return_term loc (Ast.LetIn (name, t1, t2))
+ | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
+ defs = LIST1 [
name = IDENT;
index = OPT [ LPAREN "("; index = INT; RPAREN ")" ->
int_of_string index
@@ -84,15 +138,17 @@ EXTEND
(name, t1, typ, (match index with None -> 1 | Some i -> i))
] SEP (IDENT "and");
IDENT "in"; body = term ->
- return_term loc (LetRec (defs, body))
- | typ = OPT [ LPAREN "["; typ = term; RPAREN "]" -> typ ];
- "match"; t = term; "with";
+ return_term loc (Ast.LetRec (ind_kind, defs, body))
+ | outtyp = OPT [ LPAREN "["; typ = term; RPAREN "]" -> typ ];
+ "match"; t = term;
+ SYMBOL ":"; indty = IDENT;
+ "with";
LPAREN "[";
patterns = LIST0 [
- p = pattern; SYMBOL <:unicode> (* â*); t = term -> (p, t)
+ p = pattern; SYMBOL <:unicode> (* â *); t = term -> (p, t)
] SEP SYMBOL "|";
RPAREN "]" ->
- return_term loc (Case (t, typ, patterns))
+ return_term loc (Ast.Case (t, indty, outtyp, patterns))
| LPAREN "("; t = term; RPAREN ")" -> return_term loc t
]
];
@@ -100,3 +156,209 @@ END
let parse_term = Grammar.Entry.parse term
+(*
+open Disambiguate_struct
+open ProofEngineHelpers
+
+exception UnknownIdentifier of string
+exception InductiveTypeExpected
+
+let list_of_domain dom = Domain.fold (fun s acc -> s :: acc) dom []
+let apply_interp (interp: interpretation) item = snd (interp item)
+
+let pre_disambiguate ~context ast =
+ let rec aux loc context = function
+ | Ast.LocatedTerm (loc, term) -> aux loc context term
+ | Ast.Appl terms ->
+ let (dom, funs) =
+ List.fold_left
+ (fun (dom, funs) term ->
+ let (dom', f) = aux loc context term in
+ (Domain.union dom dom', f :: funs))
+ (Domain.empty, [])
+ terms
+ in
+ let f interp =
+ Cic.Appl (List.map (fun f -> f interp) (List.rev funs))
+ in
+ (dom, f)
+ | Ast.Appl_symbol (symb, args) ->
+ let (dom, funs) =
+ List.fold_left
+ (fun (dom, funs) term ->
+ let (dom', f) = aux loc context term in
+ (Domain.union dom dom', f :: funs))
+ (Domain.empty, [])
+ args
+ in
+ (Domain.add (Symbol (symb, 0)) dom,
+ (fun interp ->
+ apply_interp interp (Symbol (symb, 0)) interp
+ (List.map (fun f -> f interp) funs)))
+ | Ast.Binder (binder_kind, var, typ, body) ->
+ let (type_dom, type_f) =
+ match typ with
+ | Some t -> aux loc context t
+ | None -> (Domain.empty, (fun _ -> Cic.Implicit))
+ in
+ let (dom', body_f) = aux loc (Some var :: context) body in
+ let dom'' = Domain.union dom' type_dom in
+ (dom'',
+ match binder_kind with
+ | `Lambda ->
+ (fun interp ->
+ Cic.Lambda (var, type_f interp, body_f interp))
+ | `Pi | `Forall ->
+ (fun interp ->
+ Cic.Prod (var, type_f interp, body_f interp))
+ | `Exists ->
+ (fun interp ->
+ let typ = type_f interp in
+ Cic.Appl
+ [ apply_interp interp (Id "ex") interp [];
+ typ;
+ (Cic.Lambda (var, typ, body_f interp)) ]))
+ | Ast.Case (term, indty_ident, outtype, branches) ->
+ let (term_dom, term_f) = aux loc context term in
+ let (outtype_dom, outtype_f) =
+ match outtype with
+ | Some typ -> aux loc context typ
+ | None -> (Domain.empty, (fun _ -> Cic.Implicit))
+ in
+ let do_branch (pat, term) =
+ let rec do_branch' context = function
+ | [] -> aux loc context term
+ | hd :: tl ->
+ let (dom, f) = do_branch' (Some (Cic.Name hd) :: context) tl in
+ (dom,
+ (fun interp ->
+ Cic.Lambda (Cic.Name hd, Cic.Implicit, f interp)))
+ in
+ match pat with
+ | _ :: tl -> (* ignoring constructor *)
+ do_branch' context tl
+ | [] -> assert false
+ in
+ let (branches_dom, branches_f) =
+ List.fold_right
+ (fun branch (dom, f) ->
+ let (dom', f') = do_branch branch in
+ Domain.union dom dom', (fun interp -> f' interp :: f interp))
+ branches
+ (Domain.empty, (fun _ -> []))
+ in
+ (Domain.union outtype_dom (Domain.union term_dom branches_dom),
+ (fun interp ->
+ let (indtype_uri, indtype_no) =
+ match apply_interp interp (Id indty_ident) interp [] with
+ | Cic.MutInd (uri, tyno, _) -> uri, tyno
+ | _ -> assert false
+ in
+ Cic.MutCase (indtype_uri, indtype_no, outtype_f interp,
+ term_f interp, branches_f interp)))
+ | Ast.LetIn (var, body, where) ->
+ let (body_dom, body_f) = aux loc context body in
+ let (where_dom, where_f) = aux loc context where in
+ (Domain.union body_dom where_dom,
+ fun interp -> Cic.LetIn (Cic.Name var, body_f interp, where_f interp))
+ | Ast.LetRec (kind, defs, where) ->
+ let context' =
+ List.fold_left (fun acc (var, _, _, _) -> Some (Cic.Name var) :: acc)
+ context defs
+ in
+ let (where_dom, where_f) = aux loc context' where in
+ let inductiveFuns =
+ List.map
+ (fun (var, body, typ, decr_idx) ->
+ let body_dom, body_f = aux loc context' body in
+ let typ_dom, typ_f =
+ match typ with
+ | None -> (Domain.empty, (fun _ -> Cic.Implicit))
+ | Some typ -> aux loc context' typ
+ in
+ (Domain.union body_dom typ_dom,
+ (fun interp ->
+ (var, decr_idx, typ_f interp, body_f interp))))
+ defs
+ in
+ let dom =
+ List.fold_left (fun acc (dom, _) -> Domain.union acc dom)
+ where_dom inductiveFuns
+ in
+ let inductiveFuns interp =
+ List.map (fun (_, g) -> g interp) inductiveFuns
+ in
+ let build_term counter funs =
+ (* this is the body of the fold_right function below. Rationale: Fix
+ * and CoFix cases differs only in an additional index in the
+ * indcutiveFun list, see Cic.term *)
+ match kind with
+ | `Inductive ->
+ (fun (var, _, _, _) cic ->
+ incr counter;
+ Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
+ | `CoInductive ->
+ let funs =
+ List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
+ in
+ (fun (var, _, _, _) cic ->
+ Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
+ in
+ (dom,
+ (fun interp ->
+ let counter = ref 0 in
+ let funs = inductiveFuns interp in
+ List.fold_right (build_term counter funs) funs (where_f interp)))
+ | Ast.Ident (name, subst) ->
+ (* TODO hanlde explicit substitutions *)
+ let rec find acc e = function
+ | [] -> raise Not_found
+ | Some (Cic.Name hd) :: tl when e = hd -> acc
+ | _ :: tl -> find (acc + 1) e tl
+ in
+ (try
+ let index = find 1 name context in
+ if subst <> [] then
+ fail loc "Explicit substitutions not allowed here";
+ (Domain.empty, fun _ -> Cic.Rel index)
+ with Not_found ->
+ (Domain.singleton (Id name),
+ (fun interp -> apply_interp interp (Id name) interp [])))
+ | Ast.Num num ->
+ (* TODO check to see if num can be removed from the domain *)
+ (Domain.singleton (Num (num, 0)),
+ (fun interp -> apply_interp interp (Num (num, 0)) interp []))
+ | Ast.Meta (index, subst) ->
+ let (dom, funs) =
+ List.fold_left
+ (fun (dom, funs) term ->
+ match term with
+ | None -> (dom, (fun _ -> None) :: funs)
+ | Some term ->
+ let (dom', f) = aux loc context term in
+ (Domain.union dom dom',
+ (fun interp -> Some (f interp)) :: funs))
+ (Domain.empty, [])
+ subst
+ in
+ let f interp =
+ Cic.Meta (index, List.map (fun f -> f interp) (List.rev funs))
+ in
+ (dom, f)
+ | Ast.Sort `Prop -> Domain.empty, fun _ -> Cic.Sort Cic.Prop
+ | Ast.Sort `Set -> Domain.empty, fun _ -> Cic.Sort Cic.Set
+ | Ast.Sort `Type -> Domain.empty, fun _ -> Cic.Sort Cic.Type
+ | Ast.Sort `CProp -> Domain.empty, fun _ -> Cic.Sort Cic.CProp
+ in
+ match ast with
+ | Ast.LocatedTerm (loc, term) ->
+ let (dom, f) = aux loc context term in
+ dom, f
+ | _ -> assert false
+
+let main ~context char_stream =
+ let term_ast = parse_term char_stream in
+ debug_print (Pp.pp_term term_ast);
+ pre_disambiguate ~context term_ast
+*)
+