From: Stefano Zacchiroli Date: Mon, 2 Feb 2004 16:43:49 +0000 (+0000) Subject: - changed ast for pattern matching so that type annotations are possible X-Git-Tag: V_0_2_3~109 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9bdc009a24ce77bf964bac758639c88647963d89;p=helm.git - changed ast for pattern matching so that type annotations are possible - bugfix for indexes in Fix/CoFix cases --- diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 3d2325c05..5a8b9a646 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -76,11 +76,12 @@ let find_in_environment name context = let interpretate ~context ~env ast = let rec aux loc context = function | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term - | CicTextualParser2Ast.Appl terms -> Cic.Appl (List.map (aux loc context) terms) + | CicTextualParser2Ast.Appl terms -> + Cic.Appl (List.map (aux loc context) terms) | CicTextualParser2Ast.Appl_symbol (symb, i, args) -> let cic_args = List.map (aux loc context) args in resolve env (Symbol (symb, i)) ~args:cic_args () - | CicTextualParser2Ast.Binder (binder_kind, var, typ, body) -> + | CicTextualParser2Ast.Binder (binder_kind, (var, typ), body) -> let cic_type = aux_option loc context typ in let cic_body = aux loc (var :: context) body in (match binder_kind with @@ -92,16 +93,19 @@ let interpretate ~context ~env ast = | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) -> let cic_term = aux loc context term in let cic_outtype = aux_option loc context outtype in - let do_branch (pat, term) = + let do_branch ((head, args), term) = let rec do_branch' context = function | [] -> aux loc context term - | hd :: tl -> - let cic_body = do_branch' (Cic.Name hd :: context) tl in - Cic.Lambda (Cic.Name hd, Cic.Implicit, cic_body) + | (name, typ) :: tl -> + let cic_body = do_branch' (name :: context) tl in + let typ = + match typ with + | None -> Cic.Implicit + | Some typ -> aux loc context typ + in + Cic.Lambda (name, typ, cic_body) in - match pat with - | _ :: tl -> (* ignoring constructor *) do_branch' context tl - | [] -> assert false + do_branch' context args in let (indtype_uri, indtype_no) = match resolve env (Id indty_ident) () with @@ -111,30 +115,41 @@ let interpretate ~context ~env ast = in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) - | CicTextualParser2Ast.LetIn (var, def, body) -> + | CicTextualParser2Ast.LetIn ((name, typ), def, body) -> let cic_def = aux loc context def in - let name = Cic.Name var in + let cic_def = + match typ with + | None -> cic_def + | Some t -> Cic.Cast (cic_def, aux loc context t) + in let cic_body = aux loc (name :: context) body in Cic.LetIn (name, cic_def, cic_body) | CicTextualParser2Ast.LetRec (kind, defs, body) -> let context' = - List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc) + List.fold_left (fun acc ((name, _), _, _) -> name :: acc) context defs in let cic_body = aux loc context' body in let inductiveFuns = List.map - (fun (var, body, typ, decr_idx) -> + (fun ((name, typ), body, decr_idx) -> let cic_body = aux loc context' body in let cic_type = aux_option loc context typ in - (var, decr_idx, cic_type, cic_body)) + let name = + match name with + | Cic.Anonymous -> + CicTextualParser2.fail loc + "Recursive functions cannot be anonymous" + | Cic.Name name -> name + in + (name, decr_idx, cic_type, cic_body)) defs in - let counter = ref 0 in + let counter = ref ~-1 in let build_term 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 *) + * inductiveFun list, see Cic.term *) match kind with | `Inductive -> (fun (var, _, _, _) cic -> @@ -145,6 +160,7 @@ let interpretate ~context ~env ast = List.map (fun (name, _, typ, body) -> (name, typ, body)) funs in (fun (var, _, _, _) cic -> + incr counter; Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic)) in List.fold_right (build_term inductiveFuns) inductiveFuns cic_body @@ -153,7 +169,8 @@ let interpretate ~context ~env ast = (try let index = find_in_environment name context in if subst <> [] then - CicTextualParser2.fail loc "Explicit substitutions not allowed here"; + CicTextualParser2.fail loc + "Explicit substitutions not allowed here"; Cic.Rel index with Not_found -> resolve env (Id name) ()) | CicTextualParser2Ast.Num (num, i) -> resolve env (Num i) ~num () @@ -185,21 +202,24 @@ let domain_of_term ~context ast = | CicTextualParser2Ast.Appl_symbol (symb, i, args) -> List.fold_left (fun dom term -> Domain.union dom (aux loc context term)) (Domain.singleton (Symbol (symb, i))) args - | CicTextualParser2Ast.Binder (_, var, typ, body) -> + | CicTextualParser2Ast.Binder (_, (var, typ), body) -> let type_dom = aux_option loc context typ in let body_dom = aux loc (var :: context) body in Domain.union type_dom body_dom | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) -> let term_dom = aux loc context term in let outtype_dom = aux_option loc context outtype in - let do_branch (pat, term) = - match pat with - | _ :: tl -> - aux loc - (List.fold_left (fun acc var -> (Cic.Name var) :: acc) - context tl) - term - | [] -> assert false + let do_branch ((head, args), term) = + let (term_context, args_domain) = + List.fold_left + (fun (cont, dom) (name, typ) -> + (name :: cont, + (match typ with + | None -> dom + | Some typ -> Domain.union dom (aux loc cont typ)))) + (context, Domain.empty) args + in + Domain.union (aux loc term_context term) args_domain in let branches_dom = List.fold_left (fun dom branch -> Domain.union dom (do_branch branch)) @@ -207,19 +227,24 @@ let domain_of_term ~context ast = in Domain.add (Id indty_ident) (Domain.union outtype_dom (Domain.union term_dom branches_dom)) - | CicTextualParser2Ast.LetIn (var, body, where) -> + | CicTextualParser2Ast.LetIn ((var, typ), body, where) -> let body_dom = aux loc context body in - let where_dom = aux loc (Cic.Name var :: context) where in - Domain.union body_dom where_dom + let type_dom = + match typ with + | None -> Domain.empty + | Some typ -> aux loc context typ + in + let where_dom = aux loc (var :: context) where in + Domain.union (Domain.union body_dom where_dom) type_dom | CicTextualParser2Ast.LetRec (kind, defs, where) -> let context' = - List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc) + List.fold_left (fun acc ((var, typ), _, _) -> var :: acc) context defs in let where_dom = aux loc context' where in let defs_dom = List.fold_left - (fun dom (_, body, typ, _) -> + (fun dom ((_, typ), body, _) -> Domain.union (aux loc context' body) (aux_option loc context typ)) Domain.empty defs in @@ -229,7 +254,8 @@ let domain_of_term ~context ast = (try let index = find_in_environment name context in if subst <> [] then - CicTextualParser2.fail loc "Explicit substitutions not allowed here"; + CicTextualParser2.fail loc + "Explicit substitutions not allowed here"; Domain.empty with Not_found -> Domain.singleton (Id name)) | CicTextualParser2Ast.Num (num, i) -> Domain.singleton (Num i)