X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fparser.ml;h=1621b3ccc254b8225e547e4a070a650d2a1fca2c;hb=970ba0021a992efe25ec374875dc127ff236cc74;hp=13f9fc42d39addc2b8cc3f7abd5fa504bb129b32;hpb=aba014724c9ad08f80944ec3021c9fa3826dca4a;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/parser.ml b/helm/ocaml/cic_disambiguation/parser.ml index 13f9fc42d..1621b3ccc 100644 --- a/helm/ocaml/cic_disambiguation/parser.ml +++ b/helm/ocaml/cic_disambiguation/parser.ml @@ -86,13 +86,14 @@ EXTEND ] | "eq" LEFTA [ t1 = term; SYMBOL "="; t2 = term -> - return_term loc (Ast.Appl_symbol ("eq", [t1; t2])) + return_term loc (Ast.Appl_symbol ("eq", 0, [t1; t2])) ] | "add" LEFTA [ (* nothing here by default *) ] | "mult" LEFTA [ (* nothing here by default *) ] | "inv" NONA [ (* nothing here by default *) ] | "simple" NONA [ + (* TODO handle "_" *) b = binder; vars = LIST1 IDENT SEP SYMBOL ","; typ = OPT [ SYMBOL ":"; t = term -> t ]; SYMBOL "."; body = term -> @@ -109,7 +110,8 @@ EXTEND | n = substituted_name -> return_term loc n | LPAREN "("; head = term; args = LIST1 term; RPAREN ")" -> return_term loc (Ast.Appl (head :: args)) - | i = INT -> return_term loc (Ast.Num i) + | i = NUM -> return_term loc (Ast.Num (i, 0)) +(* | i = NUM -> return_term loc (Ast.Num (i, Random.int max_int)) *) | m = META; substs = [ LPAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; RPAREN "]" -> @@ -156,209 +158,3 @@ 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 -*) -