]
| "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 ->
| 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 "]" ->
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
-*)
-
projects / helm.git / blobdiff